[A well-typed definition of the simply typed lambda calculus.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310040028
 + Includes a simple semantics and a normaliser which uses NBE.
 + No proofs, but everything is well-typed and structurally recursive.
] 
[Included an infinite set of base types.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310040440] 
[Added a file which imports all the other files.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310040453] 
[Added a boring file.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310040532] 
[Added minor comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310044350] 
[Renamed _++_ to _▻▻_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310130833] 
[Failed attempt at removing need for lemma by using Church encoding.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310234624] 
[Failed attempt at removing need for lemma by using Church encoding.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>*-20080310234624] 
[Renamed Semantics to Evaluation.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310234919] 
[Minor cleanup.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310235006] 
[Fixed bug in definition of η-long β-normal forms.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080311172848] 
[Listed the files in dependency order, added descriptions.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080311173234] 
[Defined a reduction semantics, along with some lemmas.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312001247] 
[Defined varToVal and valToTm.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312001301] 
[Simplified code by using Data.Star.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312005346] 
[Added _⇛⟨_⟩_ and _⟶⟨_⟩_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312133915] 
[Minor cleanup.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312134702] 
[Imported some missing modules.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312134808] 
[Added comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312210935] 
[Updated code to reflect changes in library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312210949] 
[Renamed Model to the more correct ApplicativeStructure.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080313163645] 
[Updated code to reflect changes in library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080430223335] 
[Fixed a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080710184237] 
[Updated code to reflect changes in the library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080710184614] 
[Mirrored the development using PHOAS instead of de Bruijn indices.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080710185538] 
[Added a condensed version of the HOAS.SimplyTyped modules.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080711142214] 
[Updated the code to reflect changes in Agda and the library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20090408103917
 Ignore-this: d750703da1a696ccb11e6048cb232072
] 
[Improved the documentation.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20090926123201
 Ignore-this: 6b1ea9c82a426886ada7a31c1c3d4237
] 
[Updated code to reflect changes in library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20090926123234
 Ignore-this: d566c13a5c38fa677fb7b33f6401dc7a
] 
[Clarified the status of the Semantics module.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20090926124103
 Ignore-this: 86e8379c7a40659af5044a5763ddd878
] 
[Updated code to reflect changes to library API.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101026120229
 Ignore-this: 47d2e7cd679f04565e818e3842ea17c2
]