76 citations · 373 across the 18 of their papers we have counts for
6 papers · 1 filter
foetus -- Termination Checker for Simple Functional Programs
Andreas Abel
We introduce a simple functional language foetus (lambda calculus with tuples, constructors and pattern matching) supplied with a termination checker. This checker tries to find a…
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…
Type checking through unification
Francesco Mazzoli, Andreas Abel
In this paper we describe how to leverage higher-order unification to type check a dependently typed language with meta-variables. The literature usually presents the unification a…
MiniAgda: Integrating Sized and Dependent Types
Andreas Abel
Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track s…
Semi-continuous Sized Types and Termination
Andreas Abel
Some type-based approaches to termination use sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accept…