Extending ASimple Functional Programming Language With Dependent Types
Stc
Date: 2009-11-19
Time: 12:00
Room: BBL room 471
Speaker: Robert Stremler
Title: Extending a Simple Functional Programming Language with Dependent Types
Abstract
Most programming languages that fully support dependent types require all
functions to be total. A function is total iff it is defined for any input
value and always terminates. However, dependent types are also useful in
practical programming and there totality might be a price too high.
In this talk we present and in-between solution: a functional programming
language named Pi that fully supports dependent types, but which also
allows general recursion. Starting from a simple functional programming
language, we gradually extend Pi with new concepts, eventually resulting
in a language that fully supports dependent functions, dependent datatypes
and dependently typed case constructs.
