Agda
- A dependently typed programming language
| Webpage: | Agda wiki
|
|---|
| Theory: | Dependent Type Theory
|
|---|
| Implementation: | Haskell (GHC 7)
|
|---|
| Platform: | portable
|
|---|
| Author: | Ulf Norell, Nils Anders Danielsson, Andreas Abel, and many more
|
|---|
|
My contributions to Agda:
termination checker, irrelevance, some improvements to unification, many bug fixes, ...
MiniAgda
- Termination checking using sized types
| Webpage: | MiniAgda homepage
|
|---|
| Theory: | Dependent Type Theory
|
|---|
| Implementation: | Haskell (GHC 6 and 7)
|
|---|
| Platform: | portable
|
|---|
| Author: | 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 bitbucket
|
|---|
| Theory: | Logical Framework (λΠ)
|
|---|
| Implementation: | Haskell (GHC 6 and 7)
|
|---|
| Platform: | portable
|
|---|
| Author: | 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:
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
]
| 
