[PL Seminar] Talk: Carsten Schuermann
2008.11.19 |
| Date | Mon Nov 24 |
| Time | 13:00 — 14:00 |
| Location | DI-Turing-014 |
Title: Delphin – Yet Another Way to Program with Programs.
Speaker: Carsten Schuermann, IT University of Copenhagen
Abstract:
Many different dependently typed programming languages are currently
developed invarious places, often with the promise of better
(faster, more efficient, more concise, verifiable) code. Application
areas of theses languages include general purpose programming, formal
methods, compiler construction, and automated theorem proving.
There are at least two different ways of classifying dependently typed
programming languages. The majority aims at harnessing the expressive
power of dependent types towards characterizing program invariants at
a more fine grained granular levelhoping for applications in program
verification. A fewof the languages aim at harnessing the
expressive powerof dependent types to improve the representational
capabilities with respect to modeling the world that is being
manipulated by the program.
In my talk I will report on our recently released Delphin programming
language, which falls into the latter category. Delphin is a
functional programming language supporting both higher-orderand
dependent datatypes. Type checking is decidable. Delphin is not only
a programming language but also a proof assistant for a subset of
first-order logic, in that it can fully automatically decide totality
for many programs. I my talk I motivate Delphin with examples such as
translating derivations between logical systems. Delphin and a host
of examples are available from the projectwebpage
delphin.twelf.org.
This is joint work with Adam Poswolsky.
Biographical sketch:
Since 2005 Carsten Schuermann is associate
professor and head of the PhD school at the IT University of
Copenhagen. He moved to Copenhagen from Yale University where he
started in 2000 as Assistant Professor in the Department ofComputer
Science. He received his PhD degree from Carnegie Mellon University
in 2000, his M.S. degree in 1996also from Carnegie Mellon University,
and his Diplom in Computer Science from the University of Karlsruhe in
1993.