76 citations · 373 across the 18 of their papers we have counts for
5 papers · 1 filter
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality
Andreas Abel, Thierry Coquand
Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from…
nanoBench: A Low-Overhead Tool for Running Microbenchmarks on x86 Systems
Andreas Abel, Jan Reineke
We present nanoBench, a tool for evaluating small microbenchmarks using hardware performance counters on Intel and AMD x86 systems. Most existing tools and libraries are intended t…
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…
Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
Andreas Abel, Christian Sattler
We observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped w…
Cocon: Computation in Contextual Type Theory
Brigitte Pientka, Andreas Abel, Francisco Ferreira +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…