- A dependently typed programming language
|Theory:||Dependent Type Theory
|Authors:||Ulf Norell, Nils Anders Danielsson, Andreas Abel, and many more
My contributions to Agda:
termination checker, sized types, copatterns, irrelevance, efficient projections, some improvements to unification, many bug fixes, ...
- Agda Tutorial at Proof and Computation 2016
- Autumn School
Proof and Computation
3-8 October 2016, Aurachhof, Fischbachau, Bayern, Germany
Tutorial material for live coding:
- How to Keep Your Neighbors in Order
- An Agda tutorial using Conor McBride's beautiful representation of binary search trees
30 June 2016, guest lecture in Computer Aided Formal Reasoning, class by Gordon Cichon and Martin Hofmann, Institut für Informatik, Ludwig-Maximilians-Universität München
- Agda Tutorial at FLOPS 2016
- 13th International Symposium of Functional and Logic Programming (FLOPS 2016)
6 March 2016, Kochi, Japan
Solution pretty: .html
- An Introduction to Dependent Types and Agda
- Lecture notes (7 pages) for class on functional programming.
Uses examples of vectors and sorted lists.
- Agda: Equality
- Lecture notes (6 pages) explaining definitional and propositional equality
plus syntax for equality chains.
- Verifying Program Optimizations in Agda. Case Study: List Deforestation
- Lecture notes (4 pages) demonstrating provably correct fold-unfold fusion for lists.
- Programming and Program Verification with Dependent Types in Agda
- 8 May 2012, Seminar Lehrstuhl Theoretische Informatik,
- Higher-Order Pattern Unification for Dependently Typed Records
- 1 June 2011,
TLCA 2011, 10th International Conference on
Typed Lambda Calculi and Applications, RDP 2011,
Novi Sad, Serbia.
- Sized Types in Agda
- 28 November 2008. Agda Intensive Meeting (AIM 9), Sendai, Japan.
- Frederic Kettelhoit, A Prelude for Agda (2011/12)
- Design of a prelude for the Agda standard library,
based on type classes for overloaded identifiers.
Agda Prelude auf Github
- Julien Oster, Red-Black Trees with Static Representation Invariants (2009/10)
- A dependently-typed implementation of red-black trees in Agda. Search-tree invariant and balancing are ensured by type checking.
- Parallel substitution for the untyped lambda calculus encoded with de Bruijn indices, plus correctness for substitution composition.
- Termination checking using sized types
|Theory:||Dependent Type Theory
|Implementation:||Haskell (GHC ≥ 7.6)
|Authors:||Andreas Abel, Karl Mehltretter
A Haskell implementation of a core dependently typed language with
sized types and recursive and corecursive functions. Every well-typed
program is terminating.
See MiniAgda homepage
for further information and latest release, and a blog with examples.
(The better looking MiniAgda blog has been abandoned).
- Haskell implementation of the Edinburgh Logical Framework
Helf repo on github
|Theory:||Logical Framework (λΠ)
|Implementation:||Haskell (GHC ≥ 7.8)
|Authors:||Andreas Abel, Nicolai Kraus
Helf is an implementation of the Edinburgh Logical Framework (LF) in Haskell.
The purpose is to compare term representations with regard to their efficiency
A Lambda Term Representation Based on Linear Ordered Logic
Andreas Abel and Nicolai Kraus (2011)
6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, the Netherlands, August 26, 2011.
These projects have been completed until 2003:
- Type checking Fω:
- Tool for teaching natural deduction and dependent types: Proof checker
- Termination checker based on structural ordering: