Lectures by Dexter Kozen and Dorel Lucanu

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) andDorel Lucanu (Iasi, Romania) Titles:    Dexter Kozen: Optimal Coin Flipping (abstract below)    Dorel Lucanu: Circular Behavioral Reasoning (abstract below) You are all cordially invited.
  • Lectures by Dexter Kozen and Dorel Lucanu
  • 2011-11-07T12:30:00+01:00
  • 2011-11-07T14:30:00+01:00
  • 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) andDorel Lucanu (Iasi, Romania) Titles:    Dexter Kozen: Optimal Coin Flipping (abstract below)    Dorel Lucanu: Circular Behavioral Reasoning (abstract below) You are all cordially invited.
  • When 07-11-2011 from 12:30 to 14:30 (Europe/Amsterdam / UTC100)
  • Where CWI, room L120
  • Web Visit external website
  • Add event to calendar iCal

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.