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 |
|
|
Job Search |
|
|
Publications |
|
|
Conferences |
|
|
Projects |
Curriculum Vitae
Research InterestsProgramming languages; type theory; meta-logical frameworks; automated theorem proving; formal methods; computational logic. Design of intelligent systems for the formal design and development of programming languages and logics; automated reasoning about deductive systems; design of safe programming languages and secure protocols.
Education
| 1995-present |
Carnegie Mellon University Department of Computer Science, Pittsburgh, USA. Ph.D. in Pure and Applied Logic, completion expected February 2000. Thesis: Automating the Meta Theory of Deductive Systems. Advisor: Prof. Frank Pfenning. Committee: Frank Pfenning, Robert Harper, Peter Lee, Dana Scott, Natarajan Shankar. |
| 1993-1995 |
Carnegie Mellon University Department of Philosophy, Pittsburgh, USA. M.S. in Logic and Computation, December 1995. Thesis: A Computational Meta Logic for the Horn Fragment of LF. Advisor: Prof. Frank Pfenning. Committee: Frank Pfenning, Bob Carpenter. |
| 1990-1993 |
University of Karlsruhe, Department of Computer Science, Germany. Diplom (M.S. in Computer Science), May 1993. Thesis: Design and Implementation of an Automated Theorem Prover for Linear Logic. Advisor: Prof. Jacques Calmet. Committee: Jacques Calmet, Thomas Beth. |
| 1988-1990 |
University of Karlsruhe, Department of Computer Science, Germany. Vordiplom (B.S. in Computer Science), May 1990. Thesis: OShell: A Query Language for an Object-Oriented Database System. Advisor: Prof. Gerhard Goos. |
Honors
| 1995 | Travel Grant awarded by the Association of Symbolic Logic. |
| 1993-1995 |
Doctoral fellow of the DAAD. (Doktorandenstipendium des DAAD Hochschulsonderprogramm II) |
| 1993 | Best graduating student award, University of Karlsruhe. |
| 1988 |
Fellow of the German National Scholarship Foundation. (Studienstiftung des Deutschen Volkes) |
| 1988 |
Winner of the German Federal Contest in Computer Science. (Bundeswettbewerb Informatik) |
Publications
The Meta-Logical Framework Twelf.
| [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. |
| [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. |
Teaching Experience
| Spring 1998 |
Carnegie Mellon University, Pittsburgh, USA. Teaching Assistant for Frank Pfenning's Linear Logic class. Presented four lectures and assisted students. |
| Fall 1996 |
Carnegie Mellon University, Pittsburgh, USA. Teaching Assistant for Frank Pfenning's undergraduate class, Fundamental Structures of Computer Science II. Taught recitations and assisted students. |
| Summer 1996 |
University of Darmstadt, Germany. Guest lecturerer in Frank Pfenning's Linear Logic class. Taught two classes. |
| Spring 1996 |
Carnegie Mellon University, Pittsburgh, USA. Teaching Assistant for Steve Brooke's class Programming Language Design and Processing. Taught recitations and assisted students. |
| Spring 1995 |
Carnegie Mellon University, Pittsburgh, USA. Teaching Assistant for Frank Pfenning's seminar on Linear Logic and Applications. Taught recitations and assisted students. |
| Spring 1995 |
Carnegie Mellon University, Pittsburgh, USA. Teaching Assistant for Introduction to Formal Logic. Supervised self-paced introductory undergraduate class and assisted students. |
| Fall 1994 |
Carnegie Mellon University, Pittsburgh, USA. Teaching Assistant for Teddy Seidenfeld's Logic and Computability class. Taught recitations and assisted students. |
| Sommer 1991 |
University of Karlsruhe, Germany. Teaching Assistant for Prof. Steinmetz's class Calculus II. Taught recitations and assisted students. |
| Winter 1991 |
University of Karlsruhe, Germany. Teaching Assistant for Prof. Voigt's class Calculus I. Taught recitations and assisted students. |
Conference Talks and Invited Talks
| 1999 |
System description: Twelf --- A Meta-Logical Framework for Deductive Systems. Conference on Automated Deduction, Trento, Italy. |
| 1999 |
Logical framework + Induction = Meta-logical framework. Panelist for Session Logical Frameworks and Induction, Workshop on Automation of Proofs by Mathematical Induction, Trento, Italy. |
| 1999 |
A Meta-Logical Framework for LF. Host: Thorsten Altenkirch, University of Munich, Germany. |
| 1999 |
A Meta-Logical Framework for LF. Host: David Basin, University of Freiburg, Germany. |
| 1999 |
A Meta-Logical Framework for LF. Types Workshop, Gothenburg, Sweden. |
| 1999 |
Algorithms for Equality and Unification in the Presence of Notational
Definitions. Host: Amy Felty, Lucent Technologies, Murray Hill, USA. |
| 1998 |
Automated Theorem Proving in a Simple Meta Logic for LF. Conference on Automated Deduction, Lindau, Germany. |
| 1998 |
Algorithms for Equality and Unification in the Presence of Notational
Definitions. Workshop on Proof Search for Type Theoretic Languages, Lindau, Germany. |
| 1997 |
Twelf --- an Implementation of LF Using Explicit Substitutions. Host: Tobias Nipkow, University of Munich, Germany. |
| 1997 |
Twelf --- an Implementation of LF Using Explicit Substitutions. Host: Michael Kohlhase, Saarland University, Saarbr\"ucken, Germany. |
| 1996 |
Primitive Recursion for Higher Order Abstract Syntax. Types Workshop, Aussois, France. |
| 1996 |
Primitive Recursion for Higher Order Abstract Syntax. Host: Natarajan Shankar, SRI International, Menlo Park, USA. |
| 1996 |
A Computational Meta Logic for the Horn Fragment of LF. Host: Martin Hofmann, University of Darmstadt, Germany. |
| 1995 |
Normal Proofs in Linear Logic. Logic Colloquium, Haifa, Israel. |
| 1995 |
Elf --- A Logic Programming Language? Host: Natarajan Shankar, SRI International, Menlo Park, USA. |
| 1994 |
Elf --- A Logic Programming Language? Host: Harald Rueß, University of Ulm, Germany. |
Conference Organization
| 2000 |
Chair of the Workshop on Automation of Proofs by
Mathematical Induction held in conjunction with the Conference on Automated Deduction 2000. |
Referee for Conferences and Journals
Journal of Theoretical Computer Science (TCS), Journal of Automated Reasoning (JAR), Conference on Automated Deduction (CADE), International Conference on Logic for Programming and Automated Reasoning (LPAR), Principles of Programming Languages (POPL) , Typed Lambda Calculus and Applications (TLCA), Types for Proofs and Programs (TYPES), Asian Computing Science Conference (ASIAN), Asia-Pacific Software Engineering Conference and International Computer Science Conference (APSEC/ICSC).
University Service
| Since 1999 |
Member of CMU's Speakers Club. (a committee established to review and improve student's presentation skills) |
Industry Experience
| Summer 1995 |
Intern at SRI International, Menlo Park, USA. Extended the model checking component of the theorem proving system PVS to verify specifications in LTL logic, joint work with Dr. Natarajan Shankar and Dr. Sreeranga Rajan. |
| 1990-1992 |
Research assistant at the FZI, University of Karlsruhe, Germany. Designed and implemented a query language based on the lambda calculus for the object oriented database system OBST led by Prof. Goos. |
| Winter 1989 |
Intern at the Daimler Benz Research Center Ulm, Germany. Converted the compiler-compiler CoCo from the PC platform to VAX Modula II. |
| 1985-1990 |
Freelanced at CS Computer and Software, Ulm, Germany and
Interplan, Ulm, Germany. Led group of programmers, produced administrative software for local companies. |
Personal
German citizen. Fluent in German, English, and French. Visa Status F-1.
References
|
Prof. Frank Pfenning Department of Computer Science Carnegie Mellon University 5000 Forbes Avenue Pittsburgh, PA 15213-3891 U.S.A. Office Phone: +1 412 268-6343 Office Fax: +1 412 268-5576 fp@cs.cmu.edu |
Prof. Robert Harper Department of Computer Science Carnegie Mellon University 5000 Forbes Avenue Pittsburgh, PA 15213-3891 U.S.A. Office Phone: +1 (412) 268-3675 Office Fax: +1 (412) 268-8320 rwh@cs.cmu.edu |
|
Prof. Peter Lee Department of Computer Science Carnegie Mellon University 5000 Forbes Avenue Pittsburgh, PA 15213-3891 U.S.A. Office Phone: +1 (412) 268-3049 Office Fax: +1 (412) 268-5576 petel@cs.cmu.edu |
Prof. Dana Scott Department of Computer Science Carnegie Mellon University 5000 Forbes Avenue Pittsburgh, PA 15213-3891 U.S.A. Office Phone: +1 (412) 268-3881 Office Fax: +1 (412) 268-5576 scott+@cs.cmu.edu |