1. Ambrus Kaposi
  2. tt-in-tt

Overview

HTTPS SSH

This repository contains formalisations accompanying the following papers:

  • Type Theory in Type Theory using Quotient Inductive Types (POPL 2016)

  • Normalisation by Evaluation for Dependent Types (FSCD 2016)

  • Normalisation by Evaluation for Type Theory, in Type Theory (submitted to LMCS)

by Thorsten Altenkirch and Ambrus Kaposi,

and the PhD thesis of Ambrus Kaposi titled

  • Type theory in a type theory with quotient inductive types

See Readme.agda for more information.