The Coq mailing list

[Ralph Matthes <Ralph.Matthes AT irit.fr>]

FIRST CALL FOR PARTICIPATION

WORKSHOP ON PROOFS, JUSTIFICATIONS AND CERTIFICATES

3-4 June 2016, Toulouse, France

Part of the thematic trimester CURRENT ISSUES IN THE PHILOSOPHY OF 
PRACTICE OF MATHEMATICS & INFORMATICS (CIPPMI) of the International 
Center for Mathematics and Computer Science (CIMI), University of Toulouse.

**********************************
AIMS AND SCOPE

The workshop aims to bring together researchers working in (1) 
Provability Logic, (2) Realizability, (3) Proof certificates and (4) 
Justification Logic. The aim is to foster collaboration and share ideas 
between the four fields, and all presentations will be accessible to 
researchers and students working in any of them.

There will be one session devoted to each field, each with two invited 
speakers. In order to generate a constructive exchange, aside from one 
hour of speaking time, each presentation will include an additional half 
hour devoted to questions and discussion.

*The workshop is open to all and no registration is needed.*

**********************************
PROGRAM

Friday 3rd June, Institut de Recherche en Informatique de Toulouse 
(IRIT), Auditorium Herbrand

Session 1, Friday 3rd June, 9h-10h30, 10h45-12h15, PROVABILITY LOGIC

+ Lev BEKLEMISHEV (Steklov Mathematical Institute, Russia), Positive 
provability logic and reflection calculus: an overview

+ Joost JOOSTEN (Universitat de Barcelona, Spain), A Calculus of Worms 
in Coq

Session 2, Friday 3rd June, 14h15-15h45, 16h-17h30, REALIZABILITY

+ Fernando FERREIRA (University of Lisbon, Portugal), Modified 
realizability and functional interpretations: some logical and 
mathematical observations

+ Federico ASCHIERI (Technical University of Vienna, Austria), From 
Intuitionistic Realizability to Classical Realizability

Saturday 4th June, Institut de Mathématiques de Toulouse (IMT), Amphi 
Schwartz

Session 3, Saturday 4th June, 9h-10h30, 10h45-12h15, CERTIFICATES

+ Dale MILLER (Inria Saclay, France), Defining and checking proof 
certificates

+ Jasmin Christian BLANCHETTE (Inria Nancy Grand Est, France), 
Semi-intelligible Isabelle Proofs from Machine-Generated Proofs

Session 4, Saturday 4th June, 14h15-15h45, 16h-17h30, JUSTIFICATION

+ Thomas STUDER (University of Bern, Switzerland), Justification Logic - 
a short introduction

+ Juan Pablo AGUILERA (Technical University of Vienna, Austria), An 
arithmetical interpretation for negative introspection

**********************************
WEBPAGE AND CONTACT

Workshop webpage:

http://www.cimi.univ-toulouse.fr/cippmi/en/workshop-ii-3-4th-june

You may direct inquiries to Ralph Matthes: 
matthes AT irit.fr
 .

**********************************
SCIENTIFIC COMMITTEE

+ David Fernández-Duque
+ Andreas Herzig
+ Ralph Matthes
+ Martin Strecker