76 citations · 373 across the 18 of their papers we have counts for
9 papers · 1 filter
Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda
Andreas Abel
This document provides a formal proof of Birkhoff's completeness theorem for multi-sorted algebras which states that any equational entailment valid in all models is also provable…
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…
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 in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types
Andreas Abel, James Chapman
In this paper, we present an Agda formalization of a normalizer for simply-typed lambda terms. The normalizer consists of two coinductively defined functions in the delay monad: On…
On Irrelevance and Algorithmic Equality in Predicative Type Theory
Andreas Abel, Gabriel Scherer
Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic…
Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types
Andreas Abel
Type systems certify program properties in a compositional way. From a bigger program one can abstract out a part and certify the properties of the resulting abstract program by ju…