License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
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://dagstuhl.sunsite.rwth-aachen.de/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
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI