Carsten Schürmann

 

Department of Computer Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213-3891
U.S.A.
 
carsten@cs.cmu.edu
+1.412.268.3069
+1.412.268.5576 (FAX)


  Home
  Publications
  Organization
  Projects
 

Publications


The Meta-Logical Framework Twelf.
[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.