Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
2 results

Notions of Anonymous Existence in Martin-L\"of Type Theory

Nicolai Kraus ; Martín Escardó ; Thierry Coquand ; Thorsten Altenkirch.
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these&nbsp;[&hellip;]
Published on March 24, 2017
Volume 13, Issue 1

Normalisation by Evaluation for Type Theory, in Type Theory

Thorsten Altenkirch ; Ambrus Kaposi.
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every&nbsp;[&hellip;]
Published on October 23, 2017
Volume 13, Issue 4
  • < Previous
  • 1
  • Next >