The [triangle]-Calculus. Functional Programming with Higher-Order Encodings. - Carsten Schürmann 001; Adam Poswolsky; Jeffrey Sarnat (TLCA, 2005)

Practical Programming with Higher-Order Encodings and Dependent Types. - Adam Poswolsky; Carsten Schürmann 001 (ESOP, 2008)

System Description: Delphin - A Functional Programming Language for Deductive Systems. - Adam Poswolsky; Carsten Schürmann (LFMTP@LICS, 2008)