Coinduction for semantics, analysis and verification of communicating and concurrent reactive software

This was a research project within the Estonian national ICT programme. It was run by the Institute of Cybernetics at TUT in partnership with the University of Tartu from 1 March 2013 to 31 August 2015, extended until 30 November 2015.

Ours was one of the 14 projects nationwide receiving EU structural assistance from the European Regional Development Fund within the Measure for supporting R&D in ICT (Measure 3.2.12) of the Operational programme for the development of the economic environment of the Estonian national system for the implementation of the EU Structural Funds 2007-2013.

The measure was administered by the Estonian Ministry of Education and Research and the Archimedes Foundation.

Research programme

We studied the following topics:

• Coinductive and rational types in Agda
• Monads and comonads
• Combinations of nontermination, communication and concurrency in programming language semantics and program logics
• Functional reactive programming and intuitionistic linear-time temporal logic
• Cellular automata

People

Project staff at IoC:

• Tarmo Uustalu
• Silvio Capobianco
• James Chapman
• Wolfgang Jeltsch
• Keiko Nakata
• Denis Firsov
• Niccol� Veltri
• Sandra Schumann

Project staff at U. of Tartu:

• Varmo Vene
• Kalmer Apinis
• Vesal Vojdani

External collaborators:

• Andreas Abel (Ludwig-Maximilians Univ. M�nchen → Chalmers U. of Techn.)
• Wolfgang Ahrendt (Chalmers U. of Techn.)
• Thorsten Altenkirch (U. of Nottingham)
• Venanzio Capretta (U. of Nottingham)
• Nils Anders Danielsson (Chalmers U. of Techn.)

Project meetings

• S��ritsa, 18-20 Sept. 2015
• Pillapalu, 9-11 Nov. 2014
• Kata, 21-23 Sept. 2014

Events

• Estonian-Finnish logic meeting, Rakvere, 13-15 Nov. 2015
• 21st International Conference on Types for Proofs and Programs, TYPES 2015, Tallinn, 18-21 May 2015
• 20th Agda Intensive Meeting, AIM XX, Tallinn, 16-22 October 2014
• NII Shonan meeting No. 026 on Coinduction for computation structures and programming languages, Shonan Village, Japan, 7-10 Oct. 2013

Results

See this summary.

---

Tarmo Uustalu
Last update 3 December 2015