Induction and control in type systems
4РП — Обучение и мобилност на изследователи
- Период
- 1997-10-01 → 1999-09-30
- Финансиране от ЕС
- —
- Участници
- 2
- Схема
- RGI
Линиите свързват координатора с партньорите. За проекти отпреди 2014 г. CORDIS не винаги дава точни координати. Тези точки са на ниво град или държава.
Накратко на български
Типовите системи в програмирането се анализират, за да се съчетат по-мощните механизми за разпознаване на шаблони със сложни логически структури. Това помага за създаването на по-стабилни езици за програмиране и по-надеждни системи за автоматично доказване на теореми.
Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.
Цел на проекта
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.
Оригинален текст от CORDIS (на английски).
Участници
Връзки
Данни: CORDIS, © Европейски съюз