Induction and control in type systems
FP4 — Training and Mobility of Researchers
- Duration
- 1997-10-01 → 1999-09-30
- EU contribution
- —
- Participants
- 2
- Scheme
- RGI
Lines connect the coordinator with its partners. CORDIS does not always give exact coordinates for projects before 2014. These points are placed at city or country level.
Project objective
Research objectives and content Induction Many programming languages and proof development systems are based on powerful type theories with a mechanism for inductive definitions. In programming languages, the mechanism -pattern- matching- is powerful but the type systems are logically weak. In proof development systems, the type systems are logically strong -technically, with dependent types- but the mechanism for inductive definitions -elimination principles- is not powerful enough. I propose to remedy to this mistmatch and study pattern-matching in the context of dependently typed systems -with and without subtyping. Previous work by the applicant on congruence types and the theory of labels will be crucially used to define and study the suggested type theories. Control Since 199O, many classical lambda calculi, enriching a typed lambda calculus with control oper- ators, have been studied in the literature and used to give a computationally meaningful interpretation of classical logic. One fundamental limitation of all these calculi is to be non-dependent. The question naturally arises whether the existing results scale up to systems of dependent types. A priori, the answer is far from obvious. Most of the afore cited syntaxes are tailored for non-dependent calculi and cannot be meaningfully extended to systems of dependent types. Besides, earlier work on the Calculus of Constructions has revealed anomalies with excluded middle in an impredicative type theory. Nevertheless, ongoing joint work with J. Hatcliff and M.H. S0rensen shows that it is possible to extend dependently typed systems, and more generally pure type systems, with a computationally meaningful classical operator. I propose to develop this line of work further. My main objectives are to provide a foundation for classical and computationally meaningful proof development systems and program extraction. Training content (objective, benefit and expected impact) The proposed research will enable me to deepen my knowledge in type theory, especially in the fields of induction and control. I will have ample opportunities to interact with the designers of proof development systems and to learn from the host institute expertise in theoretical and practical apsects of type theory.
Original text from CORDIS.
Participants
Links
Data: CORDIS, © European Union