License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.6
URN: urn:nbn:de:0030-drops-59727
URL: http://drops.dagstuhl.de/opus/volltexte/2016/5972/
Go to the corresponding LIPIcs Volume Portal


Altenkirch, Thorsten ; Kaposi, Ambrus

Normalisation by Evaluation for Dependent Types

pdf-format:
LIPIcs-FSCD-2016-6.pdf (0.5 MB)


Abstract

We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated using internal type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction. NBE for simple types is using a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We have formalized parts of the construction in Agda.

BibTeX - Entry

@InProceedings{altenkirch_et_al:LIPIcs:2016:5972,
  author =	{Thorsten Altenkirch and Ambrus Kaposi},
  title =	{{Normalisation by Evaluation for Dependent Types}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5972},
  URN =		{urn:nbn:de:0030-drops-59727},
  doi =		{10.4230/LIPIcs.FSCD.2016.6},
  annote =	{Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda}
}

Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda
Seminar: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 16.06.2016


DROPS-Home | Fulltext Search | Imprint Published by LZI