Carsten Schürmann 


Professor IT University of Copenhagen Rued Langgaards Vej 7 2300 Copenhagen S Denmark carsten@itu.dk 4C13 (office) ++45.72.18.52.82 (office) ++45.46.98.88.11 (home) ++45.26.39.36.06 (cell) ++45.72.18.50.01 (fax) 


Research InterestsLogic in computer science, logical frameworks, type theory, theorem proving, computational logic, functional programming languages, logic programming languages.ProjectsI 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. Newswith Florian Rabe. A Practical Module System for LF, submitted. with Jeffrey Sarnat. Lexicographic Path Induction, submitted. with Anders SchackNielsen. Linear Contextual Modal Type Theory, submitted. with Adam Poswolsky. Delphin  A Functional Programming Language for Deductive Systems, accepted to LFMTP 2008. with Anders SchackNielsen. 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 HigherOrder Encodings and Dependent Types, ESOP 2008. with Jatin Shah. Classification of Recursive Functions into Polynomial and Superpolynomial 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 metalogical frameworks at ESSLLI06: Slides for logical and metalogical frameworks at ESSLLI06: 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. MetaLogical 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 Superpolynomial Complexity Classes. Proceedings of Computer Science Logic (CSL05), 2005, Oxford, Great Britain. To appear. with MarkOliver 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 nablacalculus. Functional programming with higherorder encodings. Typed Lambda Calcului and Applications (TLCA) 2005, Nara, Japan. To appear. Slides on Twelf and Delphin: Logic and Functional programming in a metalogical framework. of an invited lecture given at FLOP 2004, Nara, Japan. Carsten Schürmann. Programming with HigherOrder Abstract Syntax. Submitted. I am organizing the 4th Workshop on Logical Frameworks and Metalanguages (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 NPComplete 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 SR200306, 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. 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 .oneCalculus: 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 TypeTheoretic Approach to Induction with Higherorder Encodings. Proceedings of Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2001), Havana, Cuba. 2001. Carsten Schürmann. Recursion for HigherOrder Encodings. Proceedings of Computer Science Logic (CSL 2001), Paris, France. LNCS 2142, pp 585599, 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. 