Here is my homepage with various stuff I've done.
2011 Implementing Substructural Logical Frameworks. PhD Thesis, January 2011. pdf
2010 The λσ-Calculus and Strong Normalization.
Technical Report TR-2010-132 in IT University Technical Report Series, October 2010.
pdf
ps
ps.gz
BibTeX
Abella src:
download
browse
2010 Curry-Style Explicit Substitutions for the Linear and Affine
Lambda Calculus. In: International Joint Conference on Automated Reasoning
(IJCAR 2010), Edinburgh, UK, July 16--19, pp. 1--14
pdf
Twelf src:
download
2010 Pattern Unification for the Lambda Calculus with Linear and Affine Types. In: 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010) Edinburgh, UK, July 14. pdf
2009 Redesigning the CLF type theory pdf
2008 Unification and Explicit Substitutions for the Linear Lambda Calculus (Master's Thesis) pdf
The substructural logical framework Celf. Celf has its own webpage.
Strong normalization of explicit substitutions in Abella tgz
(Associated Tech Report ITU-TR-2010-132.pdf)
This development is also featured as part of the Abella example collection
here,
where the proof sources can be easily browsed.
Subject reduction, confluence, and termination for explicit substitutions with linear and affine types and meta-variables in Twelf tgz
Linear Contextual Modal Logic in Twelf tgz