Opendata, web and dolomites


Infinitary Rewriting for Type Systems

Total Cost €


EC-Contrib. €






Project "InfTy" data sheet

The following table provides information about the project.


Organization address
address: NORREGADE 10
postcode: 1165

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 Coordinator Country Denmark [DK]
 Project website
 Total cost 200˙194 €
 EC max contribution 200˙194 € (100%)
 Programme 1. H2020-EU.1.3.2. (Nurturing excellence by means of cross-border and cross-sector mobility)
 Code Call H2020-MSCA-IF-2015
 Funding Scheme MSCA-IF-EF-ST
 Starting year 2016
 Duration (year-month-day) from 2016-08-01   to  2018-07-31


Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 
1    KOBENHAVNS UNIVERSITET DK (KOBENHAVN) coordinator 200˙194.00


 Project objective

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.


year authors and title journal last update
List of publications.
2018 Łukasz Czajka
A shallow embedding of Pure Type Systems into first-order logic
published pages: , ISSN: 1868-8969, DOI:
LIPIcs, vol. 97 (accepted for publication) 2019-06-13
2018 Łukasz Czajka
A new coinductive confluence proof for infinitary lambda-calculus
published pages: , ISSN: 1860-5974, DOI:
Logical Methods in Computer Science (submitted, under review) 2019-06-13
2017 Łukasz Czajka
Confluence of an extension of Combinatory Logic by Boolean constants
published pages: , ISSN: , DOI: 10.4230/LIPIcs.FSCD.2017.14
FSCD 2017, LIPIcs vol. 84 2019-06-13
2018 Łukasz Czajka, Burak Ekici, Cezary Kaliszyk
Concrete Semantics with Coq and CoqHammer
published pages: 53-59, ISSN: , DOI: 10.1007/978-3-319-96812-4_5
CICM 2018 2019-06-13
2018 Łukasz Czajka
An infinitary rewriting interpretation of coinductive types
published pages: , ISSN: 1860-5974, DOI:
Logical Methods in Computer Science (submitted, under review) 2019-06-13

Are you the coordinator (or a participant) of this project? Plaese send me more information about the "INFTY" project.

For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.

Send me an  email ( and I put them in your project's page as son as possible.

Thanks. And then put a link of this page into your project's website.

The information about "INFTY" are provided by the European Opendata Portal: CORDIS opendata.

More projects from the same programme (H2020-EU.1.3.2.)

ActinSensor (2019)

Identification and characterization of a novel damage sensor for cytoskeletal proteins in Drosophila

Read More  

STIMOS (2019)

Stimulation of Multiple Organoids Simultaneously

Read More  

OptoTransport (2019)

Light-enabled transport phenomena in van der Waals heterostructures

Read More