News

Old News

Meta-Logical Frameworks and Formal Digital Libraries. Position Paper. Verified Software: Theories, Tools, Experiments. Zurich, Switzerland. To appear.

with Jatin Shah. Classification of Recursive Functions into Polynomial and Super-polynomial Complexity Classes. Proceedings of Computer Science Logic (CSL05), 2005, Oxford, Great Britain. To appear.

with Jeffrey Sarnat. A Proof Theoretic Account of Logical Relations. Submitted. The accompanying Twelf source code can be found here.

This semester I am teaching CPSC 201: Introduction to Computer Science.

with Mark-Oliver Stehr. An Executable Formalization of the HOL/Nurpl Connection in Twelf. 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Montevideo, Uruguay. To appear.

Carsten Schürmann, Adam Poswolsky, Jeffrey Sarnat. The nabla-calculus. Functional programming with higher-order encodings. Typed Lambda Calcului and Applications (TLCA) 2005, Nara, Japan. To appear.

Information about the qualifying exams at Yale Computer Science.

Slides on Twelf and Delphin: Logic and Functional programming in a meta-logical framework. of an invited lecture given at FLOP 2004, Nara, Japan.

Carsten Schürmann. Programming with Higher-Order Abstract Syntax. Submitted.

I am organizing the 4th Workshop on Logical Frameworks and Meta-languages (LFM'04), to be held in Cork, Ireland.

Adam Poswolsky and Carsten Schürmann. Factoring Proofs. Submitted.

This Spring, I was teaching Introduction to Computer Science.

Jatin Shah and Carsten Schürmann. Representing Reductions of NP-Complete Problems in Logical Frameworks - A Case Study., Proeceedings of the MERLIN workshop, Uppsala Sweden, 2003. To appear.

Carsten Schürmann. Position Paper: Meta Logical Frameworks and QPQ. In QPQ workshop, Miami, July 2003. To appear.

Serge Autexier, Carsten Schürmann. Disproving False Conjectures. Revised version to appear at LPAR, Almaty, Kazakhstan, September 2003. An extended version is availabe as SEKI technical report SR-2003-06, University of Saarbruecken.

Andrew McCreight and Carsten Schürmann. A Meta Linear Logical Framework, draft.

Carsten Schürmann and Frank Pfenning. A Coverage Checking Algorithm for LF. Revised version to appear at TPHOLs, Roma, Italy, September 2003.

Carsten Schürmann. A regular simply type lambda calculus. Draft.

Proof Planning in Logical Frameworks, slides, colloquium given at Harvard in September 2002.

Carsten Schürmann Twelf. Lecture Notes for Summerschool "Proofs and Programs" in Eugene, Oregon, and for Summerschool "Types" in Giens, France, 2002.

Carsten Schürmann, Serge Autexier Towards proof planning for M2+. Workshop on Logical Frameworks and Metalanguages (LFM 2002), Copenhagen, Denmark, 2002. Slides.

Carsten Schürmann, Richard Fontana, Yu Liao Delphin: Functional Programming with deductive systems. Draft.

Carsten Schürmann. The .one-Calculus: Towards An Efficient Implementation of Explicit Substitutions. Proceedings of 2nd International Workshop on Implementation of Logics (IWIL 2001), Havana, Cuba. 2001.

Carsten Schürmann. A Type-Theoretic Approach to Induction with Higher-order Encodings. Proceedings of Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2001), Havana, Cuba. 2001.

Carsten Schürmann. Recursion for Higher-Order Encodings. Proceedings of Computer Science Logic (CSL 2001), Paris, France. LNCS 2142, pp 585-599, 2001.

Carsten Schürmann, Dachuan Yu, Zhaozhong Ni. A Representation of Fomega in LF. Electronic Notes in Theoretical Computer Science. Vol 58, No.1. 2001.

Hongwei Xi, Carsten Schürmann. CPS Transform and Type Derivations for Dependent ML. Wollic 2001.