#	Pagina
attuale pagina	/open-h2020/projects/202865/index.html

Opendata, web and dolomites

InfTy

Infinitary Rewriting for Type Systems

Total Cost €

EC-Contrib. €

Partnership

Views

Outcomes and
results

InfTy project word cloud

Explore the words cloud of the InfTy project. It provides you a very rough idea of what is the project "InfTy" about.

software corecursion computer ubiquitous mathematical coinductive communities exact compositional fellow calculus producing interactive infty expertise designing requests arithmetic integrating languages infinite manipulating hm combinatory formalisms types lambda investigations computations productivity construct stream adopting theoretical opening science programming theory he reasoning supervisor itself unifying infinitary typable representing ouml models extend programs endrullis simplifies list proofs input automata pure normalisation viewpoint methodology techniques confluence community objects rewriting et perspective establishing devise chosen applicable modelled typed al safe play

Project "InfTy" data sheet

The following table provides information about the project.

Coordinator	KOBENHAVNS UNIVERSITET Organization address address: NORREGADE 10 city: KOBENHAVN postcode: 1165 website: www.ku.dk 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	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

Partnership

Take a look of project's partnership.

#	participants	country	role	EC contrib. [€]
1	KOBENHAVNS UNIVERSITET KOBENHAVNS UNIVERSITET Organization address address: NORREGADE 10 city: KOBENHAVN postcode: 1165 website: www.ku.dk contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	DK (KOBENHAVN)	coordinator	200˙194.00

Map

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.

Publications

List of publications.
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.