Special edition of the ACG Colloquium organized by CWI's research group SEN3 (Foundations of Software Engineering)
In the context of the NWO project CORE: Coinductive calculi of Regular Expressions (UL, CWI), we will have the following two distinguished guests:
Dexter Kozen (Cornell, USA) and
Dorel Lucanu (Iasi, Romania)
Titles:
Dexter Kozen: Optimal Coin Flipping (abstract below)
Dorel Lucanu: Circular Behavioral Reasoning (abstract below)
You are all cordially invited.
Optimal Coin Flipping
Dexter Kozen, Cornell University
In this talk I will show how to simulate a coin of arbitrary real bias q with a coin of arbitrary real bias p with negligible loss of entropy. I will develop a coalgebraic model and use it to derive an information-theoretic lower bound that is strictly larger than the Shannon entropy. There are efficient protocols that approximate the lower bound to within any desired accuracy and achieve it exactly for p=1/2. It is an open question whether there are optimal computable protocols for any given rational p and q.
Circular Behavioral Reasoning
Dorel Lucanu, Iasi
Circular coinduction was introduced by G. Rosu and J. Goguen (IJCAR
2001, WADT 2002) as an algorithm for proving behavioral properties
expressed as indistinguishability under experiments, where the
experiments are described as particular contexts. Later, G. Rosu and
D. Lucanu formalized the circular coinduction as a proof system (CALCO
2009) and extended it with special contexts (ICFEM 2009) and
equational interpolants (ICFEM 2010). The current proof system is
implemented in CIRC tool:
http://fsl.cs.uiuc.edu/index.php/Circ
https://fmse.info.uaic.ro/projects/5/?t=info
The tool can be used for proving properties of streams, infinite binary trees, processes, regular expressions defined by polynomial functors, etc. During the development of the CIRC tool, we noticed that the same circularity principle can be applied for proving inductive properties in an automated way.
In this talk we present an abstract formalism of the circular behavioral reasoning such that the circular coinduction and circular induction are instances of this formalism. This result is somehow surprising, since the induction and the coinduction are dual notions. We also discuss some aspects regarding the combination of the two proving techniques in this formalism.
