Research Interests

Consulting

I consult regaring Zero-Trust Architectures and how update business to become compliant. Please visit our Zero-Trust Architectures webpage.

I consult regaring the use of technologies in elections. Please visit our DemTech Group webpage.

Projects

I am the principal investigator of the DemTech project, where we study how technology in elections affects the collective trust. Please visit our DemTech webpage.

I am working on the Twelf project, the Delphin project, and the Logosphere project.

News

with Florian Rabe. A Practical Module System for LF, submitted.

with Jeffrey Sarnat. Lexicographic Path Induction, submitted.

with Anders Schack-Nielsen. Linear Contextual Modal Type Theory, submitted.

with Adam Poswolsky. Delphin -- A Functional Programming Language for Deductive Systems, accepted to LFMTP 2008.

with Anders Schack-Nielsen. System Description: Celf - A Logical Framework for Deductive and Concurrent Systems, to appear at IJCAR 2008. A short talk was accepted to LICS 2008 short talks category, System Description: Celf - A Logical Framework for Deductive and Concurrent Systems.

with Jeffrey Sarnat. Structural logical relations, to appear at LICS 2008.

with Adam Poswolsky. Practical Programming with Higher-Order Encodings and Dependent Types, ESOP 2008.

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.

Slides Proof directed programming, Twelf -- a case study,, ChitChat Workshop 2006, University of Nijmegen.

Slides On the Formalization of Proofs by Logical Relations,, Workshop on the Meta Theory of Programming Languages, 2006, Portland, Oregon.

Slides for logical- and meta-logical frameworks at ESSLLI-06:

Slides for logical- and meta-logical frameworks at ESSLLI-06: Lecture 1, Lecture 2, Lecture 3, Lecture 4 and Lecture 5.

The Electronic Voting Project.

Logosphere, a formal digital library of mathematical proof. Slides. The 17th Nordic Workshop on Programming Theory. Copenhagen, Denmark. Invited talk.

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 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.

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.