[Pl-seminar] 9/10: Vilhelm Sjoberg, Dependent types with nontermination

[Vincent St-Amour]

NUPRL Seminar presents

Vilhelm Sjoberg
University of Pennsylvania

10:30 - 11:45
Wednesday, 9/10
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Dependent types with nontermination

Abstract:
Most existing dependently typed languages require all functions to be total,
and enforce this by a (necessarily conservative) termination-checker. If we
wish to add dependent types to mainstream functional programming languages
this may be too restrictive.

Here we present Zombie, a dependently typed language which makes
termination-checking optional: the programmer can decide for which parts of
the program the benefit of more precise types and opportunities for erasure
are worth the extra effort of writing provably terminating code. To handle
possible nontermination the typechecker does not automatically normalize
types, like in other dependent languages. Instead, it uses Congruence
Closure to automatically make use of equation assumptions from the typing
context.

Zombie is implemented as an elaborator into a core language. We prove that
the core langauge is type safe, and that the elaborator is
semantics-preserving and complete with respected to a declarative
specification. We have used the implementation to verify some small example
programs, e.g. term unification and backtracking SAT-solving.


------------------------------------------------------------------------------

Also, a reminder. Please fill out this doodle poll to let us know which
times you're available, so we can schedule the seminar for the rest of the
semester.

http://doodle.com/ekv7z4ixepwaweur