Computing Science Applications
Programming Languages
Properties of a functional language.
Alvaro Tasistro
. [ALF] [PS]
Subject Reduction for a small typed functional language.
Ana Bove
.
[PS]
Integrated Verification in Type Theory
(
Thorsten Altenkirch
,1996)
Infinite Objects and Graph Reduction (
Catarina Coquand
)
[PS]
Lambda-calculus with explicit substitutions. (
Catarina Coquand
,1993)
[PS]
Alfa-conversion in Simply Typed Lambda Calculus.
Ana Bove
,
Paula Severi
[PS]
Zip function. (
Daniel Fridlender
,
Mia Indrika
, 1998)
[Agda]
[PS]
[slides.PS]
Simple properties of functional programs. (
Patrik Jansson
, 1999)
[Agda]
Type-checker for simply typed lambda calcucus. (
Thierry Coquand
, 1994)
[ALF]
Algorithms
Sorting (Thorsten Altenkirch)
[ALF]
[DVI]
Integrated version of a sorting algorithm. (
Thierry Coquand
)
[ALF]
Abstract insertion sort.
Alvaro Tasistro.
1995.
[DVI]
Binomial Queues (
Björn von Sydow
)
[PS]
Linear search, Insertion sort. (
Björn von Sydow
,1994)
[PS]
Unification.
Ana Bove
,
[PS]
Concurrency
formalisation of notions from process calculus. (
Prasad
,
Pawel Paczkowski
,1994) written in ALF, now is being updated for AGDA
Bisimulation in CCS (Karlis Cerans, 1993)
[DVI]
Distributed Sorting
. (Prasad, Ed Harcourt, Joergen Andersen,1996) [ALF]
Properties of FCBS (
Martin Weichert
) [ALF]
Linguistics
Type Theoretical Grammar.
Aarne Ranta
. Oxford University Press, 1994
Grammatical Framework
.
Aarne Ranta
.
Syntactical categories via type theory.
Aarne Ranta
[ALF]
[PS]
Hardware Verification
Circuits for natural arithmetic (Magnus Andersson)
[ALF]
[PS]
Some concepts of
Ruby
specification language (Matthias Sauer,
Mary Sheeran
) [half]
Mathematics
Logic
a proof that Ackermann's function is not primitive recursive. (
Nora Szasz
, 1991)
[ALF]
[PS]
Cut-elimination for minimal logic. (
Thierry Coquand
)
[ALF]
Normalisation proof for intuitionistic propositional logic. (
Peter Dybjer
)
[ALF]
Categorical combinators for dependent types (
Peter Dybjer
)
[ALF]
Combinatorial completeness of untyped combinators. (
Veronica Gaspes
, 1992)
[ALF]
[PS]
Normalisation proof for simply typed combinators.
[ALF]
(
Veronica Gaspes
, 1992) [PS]
Constructive Completeness of Intuitionistic Predicate Logic
. (
Henrik Persson
, 1996)
[ALF]
[PS]
[Licensiate]
P. Aczel's CZF (
Makoto Takeyama
)
[Agda]
Algebra
Systems of Algebras. (
Gustavo Betarte
,
Alvaro Tasistro
, 1995). [ALF]
[PS]
Integers forms an Integral Domain. (
Gustavo Betarte
, 1993)
[ALF]
[PS]
Associativity. (
Michael Hedberg
, 1991) [ALF]
Semilattices. (Michael Hedberg)
[ALF]
Polynomial ring. (
Henrik Persson
, 1997) [Agda]
[PS]
[Ph.D.]
Zantema Problem. (
Thierry Coquand
,
Henrik Persson
, 1997) [Agda]
[PS]
Gröbner Bases. (
Thierry Coquand
,
Henrik Persson
, 1998) [Agda]
[PS]
Category Theory
Category of Sets with Universes (
Veronica Gaspes
,
Peter Dybjer
) [ALF] [PS]
Internal Type Theory (
Peter Dybjer
)
[PS]
Coherence Theorem for Monoidal Category
,
Ilya Beylin
and
Peter Dybjer
[ALF]
[PS]
Coherence for Symmetric Monoidal Category. (
Ilya Beylin
). [AGDA]
[PS]
Path Category.
Ilya Beylin
. [Agda]
[PS]
Allegory of E-Relations.
Carlos Gonzalia
, 1999
[Agda]
[PS]
E-Categories,
Qiao
) [Agda]
Formulas-as-Types-as-Objects,
Qiao
,
[Agda]
[PS]
Families to define globular sets.
Makoto Takeyama
.
[Agda]
Definition of enriched categories. Makoto Takeyama.
[Agda]
Formal Topology
Definitions and applications to domain theory, (
Jan Cederquist
, 1994)
[ALF]
[PS]
Heine-Borel covering lemma, (Jan Cederquist and Sara Negri, 1996)
[half]
[PS]
Hahn-Banach theorem (Jan Cederquist, 1997)
[half]
[PS]
Real numbers & analysis,
Jan Cederquist
,
Semantics of first order languages based on formal topology (
Henrik Persson
) [ALF]
Other branches of mathematics
The fundamental theorem of arithmetic. (
Björn von Sydow
, 1992)
[ALF]
[ALF, one file]
[PS]
Higman's lemma (
Daniel Fridlender
, 1997)
[ALF]
[PS]
Intuitionistic version of Ramsey's theorem. (
Daniel Fridlender
, 1993)
[ALF]
[PS]
Misc
Consistency in ALF (
Thorsten Altenkirch
, 1994)
[PS]
Computer based verification with ALF
. (
Thorsten Altenkirch
,1996) A course in Munich University.
a tactic for commutative monoid via 2-level approach. (
Makoto Takeyama
)
[Agda]
Libraries
ALF library (a summary of what had been done by 1994)
[ALF]
[PS]
[DVI]
[HTML]
ALF Micro library
(Thorsten Altenkirch,1995)
HALF library
(Thierry Coquand, Henrik Persson, Ilya Beylin,1996);
adopted to agda
Alfa examples
(Thomas Hallgren,1998)
Agda micro library (Catarina Coquand,1999) will become public soon
Related
The
proof editors
used in the above experiments
the first
ALF
(
Thierry Coquand
,
Lennart Augustsson
,1990)
Window ALF
(
Lena Magnusson
,
Johan Nordlander
,1994).
half
(
Dan Synek
, 1996)
AGDA
/
Alfa
(
Catarina Coquand
,
Thomas Hallgren
, 1998)
Examples performed in other systems
Coq
LEGO
Nuprl
Other Links
Proof Assistants
(Netscape directory)
Logical frameworks
(Frank Pfenning)
Formal Maths
(R B Jones)