On Thursday 2015-09-24, at 10:30, in room Byron Blanc,

Speaker: Claudio Sacerdoti Coen

Title: On the Relative Usefulness of Fireballs

Publication: Beniamino Accattoli, Claudio Sacerdoti Coen, LICS 2015.

Abstract:
In CSL-LICS 2014, Accattoli and Dal Lago showed that there is an implementation of the ordinary (i.e. strong, pure, call-by-name) lambda-calculus into models like RAM machines which is polynomial in the number of beta-steps, answering a long-standing question. The key ingredient was the use of a calculus with useful sharing, a new notion whose complexity was shown to be polynomial, but whose implementation was not explored. We study useful sharing in a call-by-value scenario, introducing a new reduction machine to reduce open terms according to call-by-value and that has only a _LINEAR_ overhead with respect to the number of beta-steps.

On Thursday 2015-07-09, at 10:30, in room F102,

Speaker: Tsvetan Chavdarov Dunchev

Title: Automation of cut-elimination in proof schemata

Abstract:

Schematising sets of objects by abstracting their general structure is an important and frequently necessary task in mathematics. In this talk will be presented a method for cut-elimination by resolution for propositional and first-order proof schemata (CERESs). Cut-elimination, introduced by Gentzen, is the most prominent form of proof transformation in logic and plays an important role in automating the analysis of mathematical proofs. The removal of cuts corresponds to the elimination of intermediate statements (lemmas) from proofs resulting in a proof which is analytic in the sense, that all statements in the proof are sub-formulas of the result. Therefore, the proof of a combinatorial statement is converted into a purely combinatorial proof. For a given proof schemata we will extract a (schematic) set of clauses which is always unsatisfiable. A resolution refutation of this set will be constructed using the notion of the resolution schemata. The obtained refutation will be used as a skeleton of a proof in normal form with at most atomic cut-formulas.

On Thursday 2015-06-11, at 10h30, in room Byron Blanc,

Speaker: Isabela Drãmnesc

Title: Proof-based Synthesis of Algorithms on Binary Trees

Abstract:

Program synthesis is currently a very active area of programming language and verification communities. We address the problem of synthesizing sorting algorithms operating on binary trees.

We develop several proof techniques by extending our previous work on the synthesis of algorithms on lists. We design appropriate induction principles and various prove-solve methods mixing rewriting with assumption-based forward reasoning and goal-based backward reasoning.

The proof techniques are implemented in the Theorema system and are used for the automatic synthesis of several sorting algorithms and for some auxiliary functions. For some of the synthesized algorithms we check the correctness in the Coq system.