H2020Индивидуална стипендия2016–2018

InfTy · Infinitary Rewriting for Type Systems

„Хоризонт 2020“ — Действия „Мария Склодовска-Кюри“

Период: 2016-08-01 → 2018-07-31
Финансиране от ЕС: 200 195 €
Участници: 1
Схема: MSCA-IF-EF-ST

Линиите свързват координатора с партньорите.

Накратко на български

Математическите методи за работа с безкрайни обекти, като непрекъснати потоци от данни в компютърните програми, се анализират чрез нови системи за типове. Това помага за създаването на по-сигурни софтуерни системи и разработването на алгоритми за проверка на тяхната коректност.

Този кратък обзор е генериран от изкуствен интелект

Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.

Резултати накратко

Infinitary Rewriting for Type Systems

Infinite objects are ubiquitous in computer science. For instance, an interactive program may be modelled as taking for input a stream (an infinite list) of requests and producing a stream of responses. Infinite objects also naturally appear in lazy functional programming languages like e.g. Haskell where infinite lazy lists may be manipulated. In theoretical computer science infinite objects play an important role e.g. in automata theory and exact real number arithmetic. Representing and reasoning about infinite computations is crucial in designing safe software systems. The objective of InfTy is to devise mathematical methods for reasoning about programs manipulating infinite objects, developing compositional typed formalisms and integrating them with infinitary rewriting techniques. Our methods are compositional and applicable to higher-order programs, while still adopting the operational perspective of rewriting. We devise an infinitary rewriting interpretation of coinductive types, i.e., of types of infinite objects. We thus provide a simple theory for type systems with infinite objects and unify previous type-based and rewriting-based work on productivity. We develop algorithms to check correctness of programs manipulating infinite objects. Recently, a coinductive approach to infinitary rewriting has been proposed by Endrullis et al., and coinductive proofs for some results in infinitary rewriting have been developed. The coinductive approach simplifies investigations in infinitary rewriting and thus it is our chosen methodology. This approach, which we further develop, is by itself of high interest.

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз

Цел на проекта

Infinite objects are ubiquitous in computer science, e.g., an interactive program may be modelled as taking for input a stream (an infinite list) of requests and producing a stream of responses. In theoretical computer science infinite objects play an important role e.g. in automata theory and exact real number arithmetic. Representing and reasoning about infinite computations is crucial in designing safe software systems.The objective of InfTy is to devise mathematical methods for reasoning about programs manipulating infinite objects, developing compositional typed formalisms and integrating them with infinitary rewriting techniques. Our methods will be compositional and applicable to higher-order programs, while still adopting the operational perspective of rewriting, thus opening up a new viewpoint on higher-order typed formalisms for corecursion. We will extend Pure Type Systems with coinductive types, providing a general yet simple theory for type systems with infinite objects and unifying previous type-based and rewriting-based work on productivity. By establishing infinitary normalisation and infinitary confluence for typable terms, we will construct Böhm models for type systems with corecursion.Recently, a coinductive approach to infinitary rewriting has been proposed by Endrullis et al., and coinductive proofs for some results in infinitary rewriting have been developed by the fellow. The coinductive approach simplifies investigations in infinitary rewriting and thus it is our chosen methodology. This approach, which we will further develop, is by itself of high interest to the rewriting community, but our work will also be relevant to the typed lambda calculus and programming languages communities. The supervisor has strong expertise in rewriting, particularly infinitary rewriting. He developed much of the theory of Infinitary Combinatory Reduction Systems crucial for the present proposal.

Оригинален текст от CORDIS (на английски).

Участници

KOBENHAVNS UNIVERSITET · KOBENHAVNКоординаторДания