Theory and applications of subtyping systems for proof development, programming, and interactive processes
4РП — Обучение и мобилност на изследователи
- Период
- 1996-07-01 → 1998-06-30
- Финансиране от ЕС
- —
- Участници
- 2
- Схема
- RGI
Линиите свързват координатора с партньорите. За проекти отпреди 2014 г. CORDIS не винаги дава точни координати. Тези точки са на ниво град или държава.
Накратко на български
Системите за подтипиране в езиците за програмиране изследват как различните типове данни се свързват помежду си, например при обектно-ориентирания дизайн. Това помага за подобряване на софтуерната спецификация, проверката на математически доказателства и управлението на паралелни процеси.
Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.
Цел на проекта
I propose to study subtyping, a primitive relation important to many different areas of computer science, including software specification, object-oriented programming, modular software design, and computer-assisted proof. My first research goal is to study subtyping systems for programming languages. Sustained research over the last decade has led recently to powerful new type systems for a broad range of object-oriented features. MY research will have applications to Standard ML1S successor ML2000 and to object calculi. My second research goal is to provide a theoretical basis for enriching proof-checking systems with subtyping. Existing proof checkers, such as LEGO, COQ, and ALF do not incorporate subtyping because we do not understand the interaction between subtyping and dependent types. I propose to study this interaction in a type system incorporating these two features. My third research goal is to investigate the applications of typing and subtyping in concurrency.
Оригинален текст от CORDIS (на английски).
Участници
- University of Cambridge · CambridgeКоординаторОбединеното кралство
- Not availableНиво градИталия
Връзки
Данни: CORDIS, © Европейски съюз