The Exp-Log Normal Form of Types and Canonical Terms for Lambda Calculus with Sums

Agda code for our ICALP 2015 submission. Download from

An interpretation of the Sigma-2 fragment of classical Analysis in System T

Agda proofs for the paper Download from

Type Directed Partial Evaluation for Level-1 Shift and Reset

Coq code for the paper

Download from Tested with Coq version 8.4beta2. Compile with "make" from the command line, or Make from the Compile menu of CoqIDE.

Browse the generated HTML documentation here.

All material released under CC BY-SA licence by Danko Ilik