Journées Nationales GEOCAL-LAC-LTP 2015

10h00	Sylvain Conchon (exposé invité) Cubicle – Design and Implementation of an SMT-based Model Checker for Parameterized Systems
11h00	Pause
11h30	Ali Assaf, Raphael Cauderlier Mixing HOL and Coq in Dedukti
12h00	Mathias Fleury Formalization of Ground Inference Systems in Isabelle
12h30	Jasmin Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel Types inductifs et coinductifs pour Isabelle/HOL
13h00	Déjeuner
14h30	Martin Bodin, Thomas Jensen, Alan Schmitt Analyzing extensible records with separation logic and abstract interpretation
15h00	Pierre Wilke, Sandrine Blazy, Frédéric Besson A concrete memory model for CompCert
15h30	Léon Gondelman Un système de types pragmatique pour la vérification déductive
16h00	Pause
16h30	Sorin Stratulat Affordable Cyclic Noetherian Induction Reasoning
17h00	Timothy Bourke Some recent improvements in modelling Loosely Time-Triggered Architectures
17h30	Clément Poncelet An interpretable Model for Interactive Music Systems

09h00	Andrew Polonsky (exposé invité) Coinductive foundations of infinitary rewriting
10h00	Benedikt Ahrens, Ralph Matthes Substitution systems revisited
10h30	Pierre Lescanne Compter les lambda termes et le mettre en bijection avec des structures combinatoires
11h00	Pause
11h30	Stéphane Graham-Lengrand Realisability semantics of abstract focussing, formalised
12h00	Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger Focusing for Nested Sequents
12h30	Delia Kesner Completeness of Call-by-Need – A Logical View
13h00	Déjeuner
14h30	Fabio Zanasi Interacting Hopf algebras: the theory of linear systems
15h00	Stefano Guerrini Questing for a Theory of Quantum Computability
15h30	Simon Perdrix, Quanlong Wang Quantum Diagrammatic Reasoning: Completeness and Incompleteness
16h00	Pause
16h30	Christophe Raffalli The power of subtyping
17h00	Paul-André Melliès Logique tensorielle et effets algébriques
17h30	Business meeting GT GeoCal et LAC
19h30	Dîner au Grand Café Foy, place Stanislas

09h00	Noam Zeilberger (exposé invité) Linear lambda calculus and the combinatorics of embedded graphs
10h00	Michele Pagani, Christine Tasson, Lionel Vaux A characterization of strong normalizability by a finiteness structure via the Taylor expansion of lambda-terms
10h30	Horace Blanc Formalizing Functions as Processes
11h00	Pause
11h30	Alice Pavaux Une interprétation ludique des types fonctionnels
12h00	Guilhem Jaber Raisonner sur l'équivalence de programmes via la sémantique des jeux opérationnelle
12h30	Charles Grellois, Paul-André Melliès A semantic study of higher-order model-checking
13h00	Déjeuner
14h00	Guillaume Bury Intégrer le simplex à la méthode des tableaux
14h30	Gabriel Scherer Un algorithme simple pour l'équivalence de lambda-termes avec sommes et type vide
15h00	Damiano Mazza Parsimonious Logic
15h30	Hubert Godfroy, Jean-Yves Marion A taste of soft-linear logic for staged computation
16h00	Fin des journées