I don't think I will get around to reading this. It is awfully dense. The
subject looks interesting though. I am not sure, but this sort of type
theory might be of importance with Laughlin wave functions. The expectation
on a 2-dim surface, either a boundary or a graphene sheet <φ(z')φ(z)> ~
-log|z' – z| leads to the Laughlin wave for ψ ~ e^{φ(z')√q}e^{φ(z)√q} and
then Z ~ |z' –-z|^q exp(¼|z'|^2), which in general is computed for a
product of these in a path integral. These products <φ(z')φ(z)> emerge from
the Baker-Campbell-Hausdorff theorem and this has some bearing with the
idea of the 2-slit experiment as a logic gate, but where now instead of
slits one has fields. However, this paper looks a bit dense to read.
LC
On Tuesday, August 6, 2019 at 5:38:54 AM UTC-5, Philip Thrift wrote:
>
>
> https://arxiv.org/abs/1905.02617 :
>
> *A Type Theory for Defining Logics and Proofs*
> Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira,
> Rebecca Zucchini
> (Submitted on 7 May 2019)
>
> We describe a Martin-Löf-style dependent type theory, called Cocon, that
> allows us to mix the intensional function space that is used to represent
> higher-order abstract syntax (HOAS) trees with the extensional function
> space that describes (recursive) computations. We mediate between HOAS
> representations and computations using contextual modal types. Our type
> theory also supports an infinite hierarchy of universes and hence supports
> type-level computation thereby providing metaprogramming and (small-scale)
> reflection. Our main contribution is the development of a Kripke-style
> model for Cocon that allows us to prove normalization. From the
> normalization proof, we derive subject reduction and consistency. Our work
> lays the foundation to incorporate the methodology of logical frameworks
> into systems such as Agda and bridges the longstanding gap between these
> two worlds.
>
> @philipthrift
>
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/everything-list/2182a490-086d-4dc1-b2af-72f3657e0711%40googlegroups.com.
