Convegno Italiano di Logica Computazionale

cilc'16, 20-22 giugno 2016

Special session

On Tuesday morning (June 21) there will be a special session on Constructivism and logic (programming) in honour of Mario Ornaghi‘s seventieth birthday. Confirmed invited speakers are:

Kung-Kiu Lau, University of Manchester: From Super Mario to X-MEN.

Abstract: In this talk I will give an overview of my own journey in software development research, a journey that started in logic programming, went through component-based development, and culminates in product families. From a model-theoretic perspective, the journey started with logical models and ended up with model-driven software development.

Michael Mendler, Otto-Friedrich Universität,  Bamberg: Synchronous Programming in Intermediate Constructive Logic.

Abstract: Cyclic and concurrent logical programs, such as those arising in asynchronous circuits or in the declarative semantics of synchronous programming languages, do not admit unique canonical execution semantics. Instead, different approaches impose different restrictions on stabilization behavior to define different classes of synchronous step reactions. Typically, these are defined by operational semantics based on scheduling policies. This is good for implementations. However, it flies in the face of the beauty of declarative programming, which is to give purely logical meaning to computations. Can we regain logical sense in synchronous reactions? We argue this is possible by replacing operational stability in the classical Boolean semantics by logical stability in intermediate constructive logics. This tentative talk will report some results in this direction, featuring intermediate constructive logics related to Gödel, Dummett and Maximova.

Helmut Schwichtenberg, Ludwig-Maximilians-Universität, Munich:  Logic for real number computation.

Abstract: Gray code (also called reflected binary code) is widely known in digital communication, due to its property that the Hamming distance between adjacent Gray codes is always 1. Based on Gray code, Tsuiki has studied an expansion of real numbers as streams of {0,1,undefined} each of which contains at most one undefined, and called it the modified Gray expansion. We consider a represention of modified Gray expansion as ordinary streams, called pre-Gray code. Through the realizability interpretation we extract programs from proofs in a theory with inductive and coinductive definitions; the realizers involve (higher type) recursion and corecursion operators. As case studies we extract real number algorithms in our setting of pre-Gray code. The correctness of the extracted programs is automatically ensured by the soundness theorem. (j.w.w. Ulrich Berger, Kenji Miyamoto and Hideki Tsuiki)