collaborators

1 paper

cs.LO2019

A Type Theory for Defining Logics and Proofs

Brigitte Pientka, David Thibodeau, Andreas Abel +2

We describe a Martin-Löf-style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOA…