My contributions to Agda: termination checker, sized types, copatterns, irrelevance, efficient projections, some improvements to unification, many improvements to user experience (UX), many bug fixes, ...

Tutorials

Correct-By-Construction Programming in Agda

14 January 2019, Tutorial at the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), Hotel Cascais Miragem, Lisbon, Portugal

Introduction to Dependent Types and Agda

2 lectures during the 8th Summer School on Formal Techniques, Menlo College, Atherton, California, USA, 21-25 May 2018.

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: 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, Ludwig-Maximilians-Universitä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 fold-unfold fusion for lists.
Source code

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. (2017-12-02)
.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). (2018-05-21)
.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 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).

 

---

 

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 Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, the Netherlands, August 26, 2011.
.pdf .ps.gz .dvi .bib

Background literature:

• Frank Pfenning, Logical Frameworks: A Brief Introduction
• Andres Löh, Conor McBride, and Wouter Swierstra, A tutorial implementation of a dependently typed lambda calculus

 

---

 

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 | Professional Service | Projects | Publications | Talks | Teaching | Supervision ]

Andreas Abel, http://www.cse.chalmers.se/~abela Last modified: 2019-01-22 17:51