[TYPES] Paper on Dependent Types in Programming

[Thorsten Altenkirch]

our (Conor McBride, James McKinna and myself) new paper is available
from my webpage:
http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf
Comments are very much appreciated.

Why Dependent Types Matter

Abstract:

  We exhibit the rationale behind the design of Epigram, a dependently
  typed programming language and interactive program development
  system using refinements of a well known program, merge sort, as a
  running example. We discuss the relationship to other proposals
  to introduce aspects of dependent types into functional programming
  languages and sketch some topics for further work in this area.

Cheers,
Thorsten


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.