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

[Vincent St-Amour]

Just a reminder, Vilhelm is speaking tomorrow at 10:30.

Vincent


At Fri, 05 Sep 2014 17:53:54 -0400,
Vincent St-Amour wrote:
> 
> 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