github.com/dankoi/metamath

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

Agda code for our ICALP 2015 submission. Download from https://github.com/dankoi/metamath/tree/master/NBE-at-ENF

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

Agda proofs for the paper arxiv.org/abs/1301.5089. Download from https://github.com/dankoi/metamath/tree/master/shift-analysis

Type Directed Partial Evaluation for Level-1 Shift and Reset

Coq code for the paper http://eptcs.web.cse.unsw.edu.au/paper.cgi?COS2013.6

Download from https://github.com/dankoi/metamath/tree/master/coq/nbe_shift_1. 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.