Explore the words cloud of the InfTy project. It provides you a very rough idea of what is the project "InfTy" about.
The following table provides information about the project.
Coordinator |
KOBENHAVNS UNIVERSITET
Organization address contact info |
Coordinator Country | Denmark [DK] |
Project website | http://www.mimuw.edu.pl/ |
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.
# | ||||
---|---|---|---|---|
1 | KOBENHAVNS UNIVERSITET | DK (KOBENHAVN) | coordinator | 200˙194.00 |
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 |
---|---|---|---|
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 (fabio@fabiodisconzi.com) 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.