| TYPE THEORY AND FUNCTIONAL PROGRAMMING A WORK PROPOSAL Gustavo Betarte (2007) | |||||||||||||||||
Abstract | |||||||||||||||||
| We propose a series of work areas related to type theory and functional programming. By type theory we mean the formulation of Martin-Lof's set theory using the theory of types as logical framework, extended with record types and subtyping. The areas presented are: the implementation of an environment for carrying out constructions in type theory, the systematic development of programming in type theory as a formal discipline and the formalization in type theory of the theory of functional programming languages. We also give a succint introduction to a theory of specifications and programs in which programs and their correctness proofs are separated but still can be built up simultaneously; we propose the implementation of a programming system for this theory too. The group of people presenting this work proposal is defined by their common interest to work together in at least one of the areas proposed. There will be people working in each of these areas in the Plata region. 1. Introdu... | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||