Category: Seminars

Talk by Claudio Sacerdoti Coen

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.

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.

Talk by Tsvetan Chavdarov Dunchev

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

Speaker: Tsvetan Chavdarov Dunchev

Title: Automation of cut-elimination in proof schemata


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.

Talk by Isabella Dramnesc

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

Speaker: Isabela Drãmnesc

Title: Proof-based Synthesis of Algorithms on Binary Trees


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.

Marelle Seminar: Proofs as documents: asynchronous interaction for Coq

On Thursday 29/01/2015, at 10h30, in room Byron Blanc,

Speaker: Carst Tankink

Title: Proofs as documents: asynchronous interaction for Coq

Abstract:Since the beginning of interactive theorem proving, the actual interaction has been a simple back-and-forth between the user and the prover, with the user providing a command the prover eagerly executes, giving feedback the user then uses to compose a new command. I will present a document-oriented model for Coq proofs (based on Wenzel’s PIDE architectures for Isabelle) that asynchronously updates the proof and processes the results from the prover. This model allows faster (parallel) processing of complete proof scripts, supports a simpler interaction model for readers of formal proofs, and gives a cleaner API for writing third party tools working on top of the proof assistant’s results. I will demonstrate the model and the interactions it allows using the jEdit plugin for Coq.

Séminaire Marelle : A Coq formalization of finitely presented modules.

On Friday 22/11/2013, at 10h30, in room Byron Beige,

Speaker: Cyril Cohen.
Joint work with: Anders Mortberg.

Title: A Coq formalization of finitely presented modules.

The use of vector spaces in homology theory does not give as precise
information as with modules. A generalization to finitely presented modules
covers computable Z-homology, which gives finer-grained topological invariants.
We formalize a construction of finitely presented modules over coherent and
strongly discrete rings and discuss its properties. This formalization gives
basic building blocks that lead to a clean definition of homology groups.

Séminaire Marelle : Types and Data types in Continuation Calculus and lambda calculus

On Wednesday 20/11/2013, at 10h30, in room Byron blanc.

Speaker: Herman Geuvers.
Joint work with: Bram Geron, Universty of Birmingham.

Title: Types and Data types in Continuation Calculus and lambda calculus.

Abstract: Continuation Calculus (CC), as defined in [1], is a model for functional
computations that aims at (1) being simple (simpler than lambda calculus
and term rewriting), (2) remaining close to actual implementations and
(3) being generic (incorporating various evaluation strategies).
The original system is untyped, but there is a standard procedure for
defining data in CC and writing functions over this data.
In the talk we present a typing system for CC and compare it with the
typing of data in lambda calculus. In lambda calculus, one has the
iterative representation of data (e.g. the Church numerals), but also
the less well-known recursive representation (e.g. the so called “Scott
numerals”). In CC, the recursive data are the “standard” ones and we
show how to type them, compute with them and reason over them.

[1] Bram Geron and Herman Geuvers — Continuation calculus,
Proceedings First Workshop on Control Operators and their Semantics,
2013, edited by: Ugo de’Liguoro and Alexis Saurin, EPTCS 127, pp 66-85.

Séminaire Marelle : Certified, Efficient and Sharp Univariate Taylor Models in COQ.

On Monday 26/08/2013, at 14h30, in room Byron Blanc.

Speaker: Érik Martin-Dorel.

Title: Certified, Efficient and Sharp Univariate Taylor Models in COQ.

We present a formalisation, within the COQ proof assistant, of
univariate Taylor models. This formalisation being executable, we get a
generic library whose correctness has been formally proved and with
which one can effectively compute rigorous and sharp approximations of
univariate functions composed of usual functions such as 1/x, sqrt(x),
exp(x), sin(x) among others. In this talk, we present the key parts of
the formalisation and we evaluate the quality of our certified library
on a set of examples.

Séminaire Marelle : Sur la théorie des types homotopiques

Sorry, this entry is only available in French.

Séminaire Marelle : Automatisation de preuves en Coq par traduction en logique du premier ordre

Sorry, this entry is only available in French.

Séminaire Marelle : Le théorème des trois cercles

Sorry, this entry is only available in French.