Carsten Schürmann
Adjunct Assistant Professor of Computer Science

Diplom in Computer Science, University of Karlsruhe, 1993
Ph.D., Carnegie Mellon University, 2000
Joined Yale Faculty 2000
Personal Homepage

Office Location: AKW 312
Telephone: 432.2349

Professor Schürmann’s research interests lie in the area of computational logic, programming language theory, and formal methods with specific emphasis on the design and application of meta-logical frameworks to reason about complex software systems. Formal methods play an important role in all aspects of software development; they provide the tools for precise and unambiguous system specification and facilitate reasoning about them. Professor Schürmann is one of the main developers of the Twelf system, which is used to specify and reason about logical systems prevalent in areas such as programming languages, operational semantics, compilers, type systems, and logics. Twelf is being used as a research and teaching tool in many universities world-wide.

Professor Schürmann’s current research interest focuses on refining meta-logical frameworks and achieving a vision of intelligent development environments. His research includes the following: mathematical and type theoretic foundations of various logical frameworks for special purpose applications, expressive meta-logics to model relevant properties about formal systems, automated reasoning techniques to verify meta-theoretic properties, and tools to transform abstract specifications into real software systems.

In ongoing work, Professor Schürmann’s group is developing program extraction techniques to facilitate code generation on demand from formal designs, such as compiler implementations and client/server architectures. To this end, his group is developing a functional programming language, which will become an integral part of an intelligent development environment. This language allows programmers to work directly with abstract data objects, such as proofs, typing derivations, and explicit execution traces. It differs from other functional languages in that it supports dependent higher-order datatypes and function definition by cases over objects of any well-formed type.

Representative Publications:
	"A type-theoretic approach to induction with higher-order encodings, Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), Havana, Cuba. December 2001. To appear.
	"Recursion for higher-order encodings, Proceedings of Computer Science Logic (CSL 2001), pp. 585-599, Paris, France, September 2001. Springer Verlag LNCS 2142.
	"System description: Twelf–a meta-logical framework for deductive systems, with F. Pfenning, Proceedings of the 16th International Conference on Automated Deduction (CADE 1999), pp. 202-206, Trento, Italy, July 1999. Springer Verlag LNAI 1632.