Agda
 A dependently typed programming language
Webpage:  Agda wiki


Theory:  Dependent Type Theory


Implementation:  Haskell (GHC)


Platform:  portable


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, ...
Tutorials
 Agda Tutorial at Proof and Computation 2016
 Autumn School
Proof and Computation
38 October 2016, Aurachhof, Fischbachau, Bayern, Germany
Tutorial material for live coding:
Prelude.agda
TreeSortBool.agda
TreeSortOrd.agda
Copatterns.agda
Solutions:
TreeSortOrdSolution.agda
CopatternsSolution.agda
Solutions pretty:
TreeSortOrdSolution.html
CopatternsSolution.html
 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, LudwigMaximiliansUniversität München
Agda code:
.html
.zip
 Agda Tutorial at FLOPS 2016
 13th International Symposium of Functional and Logic Programming (FLOPS 2016)
6 March 2016, Kochi, Japan
Slides: .pdf
Start: .agda
Solution: .agda
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.
Source code
Agda code
 Agda: Equality
 Lecture notes (6 pages) explaining definitional and propositional equality
plus syntax for equality chains.
Source code
 Verifying Program Optimizations in Agda. Case Study: List Deforestation
 Lecture notes (4 pages) demonstrating provably correct foldunfold fusion for lists.
Source code
Selected Talks
 Programming and Program Verification with Dependent Types in Agda
 8 May 2012, Seminar Lehrstuhl Theoretische Informatik,
FriedrichAlexanderUniversität Erlangen.
Agda code
 HigherOrder 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.
Student Projects
 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, RedBlack Trees with Static Representation Invariants (2009/10)
 A dependentlytyped implementation of redblack trees in Agda. Searchtree invariant and balancing are ensured by type checking.
RBTree source
Code Snippets
 ParallelSubstitution.agda
 Parallel substitution for the untyped lambda calculus encoded with
de Bruijn indices, plus correctness for substitution composition.
.agda
.html
 HereditarySubstitutionSTLC.agda
 A normalizer for simply typed lambda terms using hereditary substitution.
(20171202)
.agda
.html
 NormalizationIPL.agda
 A normalizer for full Intuitionistic Propositional Logic (IPL)
using hereditary substitution. Basically extends
HereditarySubstitutionSTLC.agda
to sum types with permutative conversions
(and product types and the empty type).
The normal form is not unique (no eta).
(20180521)
.agda
.html
MiniAgda
 Termination checking using sized types
Webpage:  MiniAgda homepage


Theory:  Dependent Type Theory


Implementation:  Haskell (GHC ≥ 7.6)


Platform:  portable


Authors:  Andreas Abel, Karl Mehltretter



A Haskell implementation of a core dependently typed language with
sized types and recursive and corecursive functions. Every welltyped
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).
Helf
 Haskell implementation of the Edinburgh Logical Framework
Webpage: 
Helf repo on github


Theory:  Logical Framework (λΠ)


Implementation:  Haskell (GHC ≥ 7.8)


Platform:  portable


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
in practice.

A Lambda Term Representation Based on Linear Ordered Logic

Andreas Abel and Nicolai Kraus (2011)
6th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP 2011, Nijmegen, the Netherlands, August 26, 2011.
.pdf
.ps.gz
.dvi
.bib
Background literature:
Completed Projects
These projects have been completed until 2003:
 Type checking Fω:
Fomega and
Church.
 Tool for teaching natural deduction and dependent types: Proof checker
Tutch.
 Termination checker based on structural ordering:
Foetus.
[ Home
 CV
 Projects
 Publications
 Talks
 Teaching
 Sharing
]
