On Definability and Normalization by Evaluation in the Logical Framework
Ladda ner
Typ
Examensarbete för masterexamen
Program
Publicerad
2019
Författare
Ramcke, Frederik
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
The question of definability asks to characterise what objects of the meta-theory
are definable by a given calculus; for example, the untyped -calculus characterises
exactly the Turing-computable functions.
This thesis gives a characterisation of LF-definability—definability in a variant of
the Edinburgh Logical Framework—in terms of a notion of Kripke predicates. The
constructions in this thesis are heavily inspired by, and generalise, those by Jung
and Tiuryn, who gave a definability result for the simply-typed -calculus in ‘A New
Characterization of Lambda Definability’.
Beskrivning
Ämne/nyckelord
Definability , Logical Framework , Normalization by Evaluation , NbE