On Definability and Normalization by Evaluation in the Logical Framework
| dc.contributor.author | Ramcke, Frederik | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för data och informationsteknik | sv |
| dc.contributor.examiner | Danielsson, Nils Anders | |
| dc.contributor.supervisor | Abel, Andreas | |
| dc.date.accessioned | 2020-09-21T07:56:30Z | |
| dc.date.available | 2020-09-21T07:56:30Z | |
| dc.date.issued | 2019 | sv |
| dc.date.submitted | 2020 | |
| dc.description.abstract | 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’. | sv |
| dc.identifier.coursecode | DATX05 | sv |
| dc.identifier.uri | https://hdl.handle.net/20.500.12380/301744 | |
| dc.language.iso | eng | sv |
| dc.setspec.uppsok | Technology | |
| dc.subject | Definability | sv |
| dc.subject | Logical Framework | sv |
| dc.subject | Normalization by Evaluation | sv |
| dc.subject | NbE | sv |
| dc.title | On Definability and Normalization by Evaluation in the Logical Framework | sv |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.uppsok | H |