Extending ASimple Functional Programming Language With Dependent Types
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.