Carsten Schürmann

 

Department of Computer Science
Yale University
51 Prospect St.
New Haven, CT 06520-8285
U.S.A.
 
carsten@cs.yale.edu
+1.203.432.2349
+1.203.432.0593 (FAX)


  Home
  Publications
  Organization
  Projects
  Teaching
 

Publications


Drafts.
[S01b] Carsten Schürmann. Induction Principles for Higher-Order Abstract Syntax. submitted.

The Meta-Logical Framework Twelf.
[S01a] Carsten Schürmann. Recursion for Higher-Order Encodings. Proceedings of Computer Science Logic (CSL 2001), Paris, France. LNCS 2142, pp 585-599, 2001
[S00b] Carsten Schürmann. Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, 2000. CMU- CS-00-146.
[S00a] Carsten Schürmann. A Meta Logical Framework Based on Realizability. Workshop on Logical Frameworks and Meta-Languages (LFM 2000), Santa Barbara, California, June 2000.
[PS99] Frank Pfenning and Carsten Schürmann. System description: Twelf --- a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202--206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.
[PS98c] Frank Pfenning and Carsten Schürmann. Twelf User's Guide, 1.2 edition, September 1998. Available as Technical Report CMU-CS-98-173, Carnegie Mellon University.
[SP98] Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286--300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421.
[Sch98] Carsten Schürmann. Automating the meta theory of deductive systems. Thesis Proposal, Carnegie Mellon University, December 1998.
[Sch95] Carsten Schürmann. A computational meta logic for the Horn fragment of LF. Master's thesis, Carnegie Mellon University, December 1995. Available as Technical Report CMU-CS-95-218.

Notational Definitions.
[PS98b] Frank Pfenning and Carsten Schürmann. Algorithms for equality and unification in the presence of notational definitions. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types for Proofs and Programs. Springer-Verlag LNCS 1657, 1998. Extended version of [PS98a].
[PS98a] Frank Pfenning and Carsten Schürmann. Algorithms for equality and unification in the presence of notational definitions. In D. Galmiche, editor, Proceedings of the CADE Workshop on Proof Search in Type-Theoretic Languages. Electronic Notes in Theoretical Computer Science, July 1998.

The Modal Lambda-Calculus.
[SDP00] Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning. Primitive recursion for higher-order abstract syntax. Theoretical Computer Science, 2000. Journal version of [DPS97]. To appear.
[DPS97] Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In R.~Hindley, editor, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97), pages 147--163, Nancy, France, April 1997. Springer-Verlag LNCS. An extended version is available as Technical Report CMU-CS-96-172, Carnegie Mellon University.
[DPS96] Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. Technical Report CMU-CS-96-172, Carnegie Mellon University, September 1996.

Linear Logic.
[Sch93] Carsten Schürmann. Entwurf und Implementierung eines auf Linearer Logik basierenden Theorembeweisers. Master's thesis, University of Karlsruhe, 1993.