Link identifier archive #link-archive-thumb-soap-7332
Mercoledì 10 aprile alle ore 16.00, nell'ambito dei Junior Seminars, Adrien Ragot (dottorando, Universitè Paris Nord) terrà il seminario dal titolo "Realisability: from constructive proofs to program specification".
Abstract: In a first part - after recalling some basics of proof theory, namely what is a formal proof - we will introduce the key concept of Realisability. The Brouwer-Heyting-Kolmogorov (BHK) interpretation of proofs - originally formulated for intuistionistic logic - describes fundamental properties that should enjoy proofs. In particular it implies that the space in which proofs lives should be equipped with a product and a notion of interaction. Realisability is the implementation of the BHK-interpretation inside an untyped model of computation - first inside recursive function, variants of the lambda calculus and more recently in the context of linear logic in sets of permutations, operators on an Hilbert space, or weighted graphs. We will point out how the first versions of Realisability fall short if one wants to adopt an interactive approach and how this limit relates to consistency. We exhibit the existing modern solutions that constitutes Interactive Realisability, briefly we expose how interactive realisability is relevant for program specification. In a second part, we will present parts of our current work on Realisability for Linear Logic. We show how a simple algebraic structure, a polarized self-operand, is suited to realize multiplicative linear logic. We relate the problem of completeness in realisability to the correctness criterions of proof structures for Linear Logic. In order to study correctness, we present an algebraic framework of "path algebra" to study the connectedness and acyclicity of a graph. If times allow we will discuss in particular how one can handle second order quantifiers.
Il seminario è organizzato dai dottorandi di Matematica e si svolgerà in presenza presso il Dipartimento di Matematica e Fisica, Lungotevere Dante 476, aula M3.
