Chocola – Rencontres

In relation with the current social movement about the reform of pensions, the planned meeting is canceled -- - voir la motion adoptée par le GT Scalp.

Peter Dybjer (Chalmers Univ. (Sweden)), Generalized Algebraic Theories and Categories with Families
Axel Kerinec (LIPN), TBA
Gabriele Vanoni (INRIA), TBA

Rencontre, 26 janvier 2023

La rencontre se tiendra à l'ENS de Lyon, site Monod, en amphi B le matin, et en amphi J l'après-midi.

Zeinab Galal (LIP6, Sorbonne Université), Bidimensional fixpoint operators
Meven Lennon-Bertrand (Cambridge Univ. (UK)), Bidirectional typing is not just an implementation technique
Yannick Zakowski (INRIA (Lyon)), Monadic Definitional Interpreters as Formal Semantic Models of Computations

Rencontre, 24 novembre 2022

This meeting took place in Paris.

Giulio Guerrieri (LIS, Aix-Marseille Université), The theory of call-by-value solvability
Hugo Herbelin (INRIA), Computing with Gödel’s completeness theorem: Weak Fan Theorem, Markov’s Principle and Double Negation Shift in action
Daniela Petrisan (IRIF), Semialgebras and Weak Distributive Laws

Rencontre, 20 octobre 2022

Martin Baillon (Gallinette, LS2N), Gardening with the Pythia, A model of continuity in a dependent setting
Marie Fortin (IRIF, CNRS), FO = FO^3 for Linear Orders with Monotone Binary Relations
Tito Nguyễn (LIP, ENS de Lyon), A transducer model for simply typed λ-definable functions

Rencontre, 22 septembre 2022

Romain Couillet (Université Grenoble-Alpes), Pourquoi et comment démanteler l'IA et le numérique?
Claudia Faggian (CNRS - IRIF), Bayesian Networks and Proof Nets: Curry-Howard meets Bayes
Guillaume Geoffroy (IRIF), A first-order completeness result about characteristic Boolean algebras in classical realizability

Rencontre, 2 juin 2022

Valentin Blot (INRIA), A direct computational interpretation of second-order arithmetic via update recursion
Louise Dubois de Prisque (LMF, Inria), Sniper, a general proof automation tactic in Coq
Yannick Forster (Gallinette, Nantes), Synthetic Computability in Constructive Type Theory

Rencontre, 5 mai 2022

Le lendemain, vendredi 6 mai, se tiendra une journée du projet ANR Reciprog, à Lyon, son programme est ici.

Nathanaëlle Courant (INRIA), Testing convertibility in parallel
Gianluca Curzi (Università di Torino), Cyclic implicit complexity
Farzad Jafarrahmani (IRIF), Linear logic with fixpoints from a Curry-Howard perspective.

Rencontre, 31 mars 2022

Abhishek De (IRIF), Provability of linear logic with fixed points
Cristina Matache (Oxford University, UK), A unified treatment of concrete sheaf models for higher-order recursion
Federico Olimpieri (University of Leeds, UK), Categorifying graph models of lambda calculus

Rencontre, 10 mars 2022

Marie Kerjean (CNRS - LIPN), ∂ is for Dialectica
Denis Kuperberg (CNRS - LIP), Positive First-order Logic on Words and Graphs
Loïc Pujet (Gallinette, INRIA), Extensionality in intensional type theory

Séminaire en ligne, 20 janvier 2022

Bruno Dinis (Universidade de Lisboa, Portugal), Functional interpretations and applications

Séminaire, 2 décembre 2021

La rencontre aura lieu en amphi B, à l'ENS de Lyon. Les exposés seront diffusés en ligne. Merci de vous inscrire si vous comptez être sur place à Lyon.

Francesco Gavazzo (Università di Bologna), A Relational Theory of Effects and Coeffects
Luca Reggio (Oxford University), Game comonads: towards an axiomatic theory of resources
Alexandra Silva (Cornell University), Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks

Séminaire en ligne, 21 octobre 2021

Armaël Guéneau (Aarhus), Program verification on a capability machine in the presence of untrusted code

Séminaire en ligne, 1 juillet 2021

Daniele Varacca (LACL - Univ Paris Est Creteil), Milner and Alur walk into a bar

Séminaire en ligne, 17 juin 2021

Sonia Marin (University College London), Focused nested calculi applied to the logic of bunched implications

Attention, 15h françaises !, 3 juin 2021

Carlo Angiuli (Carnegie Mellon University), Internalizing Representation Independence with Univalence

Séminaire en ligne, 20 mai 2021

Valeria Vignudelli (ENS de Lyon), Monads, equational theories, and metrics for nondeterministic and probabilistic systems

Séminaire en ligne, 6 mai 2021

Barbara König (Universität Duisburg-Essen), Fixpoint Theory -- Upside Down

Séminaire en ligne, 22 avril 2021

Gabriele Vanoni (Università di Bologna), The Time and Space of Interaction

Séminaire en ligne, 8 avril 2021

Daniel Gratzer (Aarhus University), Sketching type theories

Séminaire en ligne, 11 mars 2021

Assia Mahboubi (Inria Gallinette, Nantes), Machine-Checked Computer-Aided Mathematics

Séminaire en ligne, 25 février 2021

Zeinab Galal (IRIF, Univ. Paris Diderot), Stable Species of Structures

Séminaire en ligne, 11 février 2021

Enguerrand Prebet (ENS de Lyon), Sequentiality, References and Well-bracketing in the pi-calculus

Séminaire en ligne, 28 janvier 2021

Benoît Montagu (Inria), Stable Relations and Abstract Interpretation of Higher-Order Programs

Séminaire en ligne, 14 janvier 2021

Giulio Manzonetto (LIPN, Université Paris-Nord), About the power of Taylor expansion

Séminaire en ligne, 17 décembre 2020

Jérémie Koenig (Yale University), Refinement-Based Game Semantics for Certified Components

Séminaire en ligne, 3 décembre 2020

Nicolas Blanco (Riverlane - University of Birmingham), Bifibrations of polycategories and classical linear logic

Séminaire en ligne, 19 novembre 2020

Paolo Pistone (Università di Bologna), The Yoneda Reduction of Polymorphic Types

Séminaire en ligne, 25 juin 2020

Delia Kesner (IRIF, Univ. Paris Diderot), The bang calculus, revisited

Séminaire en ligne, 11 juin 2020

Cyrille Chenavier (Johannes Kepler University (Linz, Austria)), Topological rewriting systems applied to standard bases and syntactic algebras

Rencontre, 14 mai 2020

Rencontre annulée du fait de la crise sanitaire

Neel Krishnaswami (University of Cambridge (UK)), TBA
Cristina Matache (Oxford University (UK)), Program Equivalence for Algebraic Effects and Higher-order Functions

Rencontre, 13 mars 2020

un vendredi!

le matin : pause café devant l'amphi B (comme toujours), puis on va en amphi K ; l'après-midi : amphi A

Amina Doumane (CNRS, ENS de Lyon), Completeness for Identity-free Kleene Lattices
Giulio Guerrieri (University of Bath (UK)), Factorization, Normalization and all that.
Damiano Mazza (CNRS, Univ. Paris 13), Automatic Differentiation in PCF

Rencontre, 6 février 2020

Rencontre annulée du fait des mouvements sur la LPPR et sur les retraites.

Cyrille Chenavier (Johannes Kepler University (Linz, Austria)), Topological rewriting systems applied to standard bases and syntactic algebras
Damiano Mazza (CNRS, Univ. Paris 13), Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Luc Pellissier (INRIA and École Polytechnique), Glueability of resource proof-structures: inverting the Taylor expansion

Séminaire, 14 novembre 2019

La rencontre se déroulera en amphi B, 3ème étage, site Monod, ENS de Lyon.

Francesco Gavazzo (IMDEA Software Institute), Differential Logical Relations
Marie Kerjean (INRIA Nantes), Higher-Order Distributions for Differential Linear Logic
Yann Régis-Gianas (IRIF, Univ. Paris Diderot), Towards certified incremental functional programming

Séminaire, 17 octobre 2019

The meeting will take place in amphi B, ENS de Lyon, Monod site (3rd floor).

On this meeting, ChoCoLa is glad to be a partner of the LHC and Scalp working groups of the GDR IM of the CNRS, and is sorry for the multiple acronyms.

Here is the announcement for the LHC meeting, and here for the SCALP meeting.

Moreover, the PhD defense of Aurore Alcolei will take place at 5:00pm after the meeting.

Nota: For this meeting, we are only able to offer the lunch. Registration should be done via this form.

Please write to chocola-gestion@ens-lyon.fr if you have difficulties funding your trip, and would like to attend.

Danel Ahman (University of Ljubljana (Slovénie)), Interacting with the external world using comodels (aka runners)
Eric Finster (Gallinette, INRIA), An opetopic syntax for higher monoidal closed categories
Dan Ghica (University of Birmingham), The next 700 abstract machines
Valeria Vignudelli (École Normale Supérieure de Lyon), The Theory of Traces for Systems with Nondeterminism and Probability

Séminaire, 26 septembre 2019

The meeting will take place in Amphi B, 3rd floor, site Monod, ENS de Lyon.

Pierre Clairambault (CNRS, ENS de Lyon), Fix Your Semantic Cube Using This Simple Trick
Andrea Condoluci (University of Bologna (Italy)), Sharing Equality is Linear
Hugo Férée (IRIF, Univ. Paris Diderot), Contributing to Higher Order Complexity: Outcomes and Likely Applications

Rencontre, 6 juin 2019

Ohad Kammar (University of Edinburgh), A tutorial on quasi-Borel spaces
Jérémy Ledent (LIX, École Polytechnique), Geometric semantics for asynchronous computability
Lutz Strassburger (INRIA Saclay and LIX, École Polytechnique), Introduction to Combinatorial Proofs

Rencontre, 9 mai 2019

Radu Mardare (Aalborg University (DK)), Non-standard semantics for stochastic computational phenomena
Daniela Petrisan (IRIF, Univ. Paris Diderot), Up-To Techniques for Behavioural Metrics via Fibrations
Mathys Rennela (LIACS, Leiden University, NL), Operator algebras in categorical quantum foundations

Rencontre, 4 avril 2019

Raphaëlle Crubillé (IRIF, Univ. Paris Diderot), Probabilistic Stable Functions on Discrete Cones are Power Series.
Xavier Leroy (Collège de France, INRIA), Formal verification of a static analyzer: abstract interpretation in type theory
Ludovic Patey (CNRS, Institut Camille Jordan), Introduction to reverse mathematics

Rencontre, 14 mars 2019

Les exposés auront lieu en Amphi B, site Monod de l'ENS de Lyon (46 allée d'Italie), 3è étage.

Ambroise Lafont (IMT Atlantique), Higher-order Arities, Signatures and Equations via Modules
Étienne Miquey (Gallinette, INRIA), A constructive proof of dependent choice in classical arithmetic via memoization
Filip Sieczkowski (University of Wrocław), Abstraction and equational reasoning for algebraic effects and handlers

Rencontre, 24 janvier 2019

Aurore Alcolei (ENS de Lyon), Resource-tracking concurrent games
Paul-André Melliès (CNRS - Univ. Paris Diderot), Template games: a homotopy model of differential linear logic
Andreas Nuyts (KU Leuven (Be)), Degrees of Relatedness

Rencontre, 13 décembre 2018

Accueil devant l'amphi B (3è étage)

Exposé du matin : salle B1 (4è étage)

L'après-midi : amphi B (3è étage)

Tom Hirschowitz (CNRS - Univ. Savoie Mont Blanc), Familial monads and structural operational semantics
Lê Thành Dũng Nguyễn (Université Paris 13), Around finite semantics for second-order multiplicative linear logic
Paolo Pistone (Tübingen Univ. (DE)), Coends and proof equivalence in second order multiplicative linear logic

Salidou day, 15 novembre 2018

This meeting will take place in Paris. We will celebrate the addition of new members to the Chocola gang, from Nantes: the Gallinette research team.

The meeting will take place in Bâtiment Sophie Germain, here.

We will first gather at the 3rd floor of the building, for a breakfast.
We will then move for the talk of the morning (11.00-12.30) to Amphi Turing.
We will have lunch in room 3052
In the afternoon (14h-16h30), we will be in room 1016

Flavien Breuvart (Université Paris 13), Graded Types Parametricity : Principles and Application to Abstract Interpretation
Xavier Leroy, Leçon inaugurale au Collège de France
Shane Mansfield (Univ. of Oxford), An overview of empirical models
Éric Tanter (Universidad de Chile & Inria Paris), Abstracting Gradual Typing: Principles and Application to Gradual Parametricity

Rencontre, 20 septembre 2018

La rencontre aura lieu en Amphi B (3ème étage, site Monod)

Henning Basold (CNRS - ENS de Lyon), Foundations for Corecursive Proof Search with Horn Clauses
Guillaume Geoffroy (Institut de Mathématiques de Marseille), Connecting degrees of parallelism and Boolean algebras through classical realizability
Thomas Streicher (Univ. Darmstadt (DE)), How Unique are Ground Models

Rencontre, 17 mai 2018

Amphi B, ENS de Lyon, site Monod

Florian Faissole (LRI), Synthetic topology in homotopy type theory for probabilistic programming
Luca Padovani (Università di Torino), Mailbox Types for Unordered Interactions
Tarmo Uustalu (Reykjavik University and Tallinn Univ. of Technology), A Coalgebraic View of Bar Recursion and Bar Induction

Rencontre, 12 avril 2018

Jean-Simon Lemay (University of Oxford (UK)), Differential Algebras for Differential Categories
Jamie Vicary (University of Oxford (UK)), Practical higher-dimensional algebra
Glynn Winskel (Cambridge University, UK), Distributed Probabilistic Strategies

Rencontre, 15 mars 2018

La rencontre aura lieu à Lyon, dans un amphi à préciser.

Bérénice Delcroix-Oger (IRIF, Univ. Paris Diderot), Why operads can be seen as enhanced species and what they are used for.
Marcelo Fiore (University of Cambridge, UK), An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures
Samuel Mimram (École Polytechnique), Mechanized tools for higher categories

Rencontre, 8 février 2018

Amphi B, ENS de Lyon, site Monod

Thomas Ehrhard (IRIF, Univ. Paris Diderot), Stable and measurable functions on positive cones: a model of probabilistic functional languages with continuous types
Justin Hsu (University College London, UK), From Couplings to Probabilistic Relational Program Logics
Prakash Panangaden (Mc Gill University, Canada), Quantitative Equational Logic

Rencontre, 14 décembre 2017

Nous serons en amphi B (site Monod, 3ème étage)

Jean Krivine (IRIF, Univ. Paris Diderot), Incremental Update for Graph Rewriting
Kenji Maillard (INRIA), F*, from practice to theory
François Pottier (INRIA), Looking back on Mezzo: experience and metatheory

Rencontre, 9 novembre 2017

Jules Chouquet (IRIF, Univ. Paris Diderot), A result concerning the size of proof-nets, and two applications
Laura Fontanella (I2M, Aix-Marseille), Realizability: from Curry-Howard to forcing
Thomas Seiller (DIKU, Univ. Copenhagen), Towards a geometric theory of computation(al complexity)

Rencontre, 12 octobre 2017

La rencontre aura lieu en amphi B.

André Joyal (Univ. Québec à Montréal), Opérades et 2-géométrie algébrique
Damiano Mazza (CNRS, LIPN), A Tour Around Polyadic Approximations
Luc Pellissier (ENS de Lyon), Linear approximations, intersection types and the Grothendieck construction

Rencontre, 29 juin 2017

Amphi A le matin, amphi B l'après-midi.

Valentin Blot ( Queen Mary University of London), An interpretation of system F through bar recursion
Marco Gaboardi (University at Buffalo, SUNY), A semantic account of metric preservation in presence of probabilities.
Marie Kerjean (IRIF), Smooth models of Differential Linear Logic

Rencontre, 11 mai 2017

La rencontre se tiendra en amphi B, 3ème étage, site Monod de l'ENS de Lyon.

Paul Blain Levy (University of Birmingham), Contextual isomorphisms
Pierre-Marie Pédrot (University of Ljubljana), An Effectful Way to Eliminate Addiction to Dependence
Christine Tasson (IRIF, Univ. Paris Diderot), Probabilistic Call by Push Value

Rencontre, 13 avril 2017

La rencontre aura lieu en amphi B, au 3è étage, sur le site Monod de l'ENS de Lyon (fléchage depuis l'ascenseur).

Jérémie Chalopin (Université Aix-Marseille), Un contre-exemple à la conjecture de Thiagarajan sur les structures d'évènements régulières
Thomas Leventis (Institut de Mathématiques de Marseille), Full abstraction of the probabilistic Böhm trees
Pierre-Yves Strub (École Polytechnique), Proving Differential Privacy via Probabilistic Couplings

Rencontre, 9 mars 2017

La rencontre se tiendra en amphi B, à l'ENS de Lyon.

Matteo Mio (CNRS, Lyon), Riesz Modal Logic for Markov Processes
Hugo Paquet (Cambridge), Concurrent game semantics for Probabilistic PCF and relational collapse
Benoît Valiron (CentraleSupélec & LRI), A Geometry of Interaction for Quantum Computation

Rencontre, 9 février 2017

La rencontre aura lieu à l'ENS de Lyon, site Monod, en amphi B (3ème étage).

Danko Ilic, Exp-log normal form of types and formulas
Olivier Laurent (CNRS, ENS de Lyon), On the Proof Theory of BCD Intersection Subtyping
Gabriel Scherer (Northeastern University, Boston), Full abstraction for language design

Rencontre, 12 janvier 2017

La rencontre aura lieu en salle B2 (4ème étage, ENS de Lyon)

Pierre Pradic (ENS de Lyon), The Logical Strength of Büchi's Decidability Theorem
Christophe Raffalli (Univ. Savoie Mont Blanc), About SubML
Lionel Vaux (Univ. Aix-Marseille), Normaliser le développement de Taylor des λ-termes

Séminaire, 1 décembre 2016

The meeting will take place

. in the morning, in room B1 (4th floor, Monod site, ENS de Lyon)

. in the afternoon, in amphi B (3rd floor, Monod site, ENS de Lyon)

Andrej Dudenhefner (Univ. Dortmund), Intersection Type Calculi of Bounded Dimension
Tom Hirschowitz (HDR, Univ. Savoie), Shapely monads and analytic functors
Pierre Vial (Université Paris 13), Some Uses of Infinitary Sequential Intersection

Rencontre, 10 novembre 2016

Cette journée CHoCoLa aura pour cadre la rencontre LL2016 - Linear Logic: interaction, proofs and computation.

Vous pouvez consulter le programme (cliquez sur une session pour avoir les détails).

La rencontre aura lieu dans la salle 1 place de l'École de l'ENS Lyon.

Rencontre, 9 novembre 2016

Cette journée CHoCoLa aura pour cadre la rencontre LL2016 - Linear Logic: interaction, proofs and computation.

Vous pouvez consulter le programme (cliquez sur une session pour avoir les détails).

La rencontre aura lieu dans la salle 1 place de l'École de l'ENS Lyon.

Séminaire, 13 octobre 2016

La rencontre aura lieu en amphi B, à l'ENS de Lyon.

Valentin Blot (University of Bath), Hybrid realizability for intuitionistic and classical choice
Jim Laird (University of Bath), Weighted Models for Computation and Communication
Marco Peressotti (Univ. of Udine), Coalgebraic Semantics of Self-Referential Behaviours

Séminaire, 22 septembre 2016

Matin : amphi B

Après-midi : amphi A (3è étage, à l'autre bout du couloir par rapport à l'amphi B)

Henning Basold (Radboud University), Dependent Inductive-Coinductive Types: Category Theoretical and Syntactic Perspectives
Pierre Hyvernat (Université de Savoie Mont Blanc Tomme Diot), Using the Size-Change Principle for checking totality of recursive definitions
Guilhem Jaber (IRIF, Univ. Paris 7), SyTeCi: Symbolic, Temporal and Circular reasoning for automatic proofs of contextual equivalence

Séminaire, 9 juin 2016

Guillaume Brunerie (Université Nice Sophia Antipolis), Examples of closed natural numbers in homotopy type theory
Thierry Coquand (University of Gothenburg (SE)), Une justification de l’axiome d’univalence
Thomas Streicher (Univ. Darmstadt (DE)), Effective Spectral Theorem for Bounded Self Adjoint Operators (tbc)

Séminaire, 12 mai 2016

We will be in Amphi B, third floor.

Simon Castellan (ENS Lyon), The parallel intensionally fully abstract model for PCF
Tom Hirschowitz (Univ. Savoie Mont Blanc), A sheaf-based approach to concurrent innocent strategies
Andrzej Murawski (Warwick University (UK)), Contextual approximation and higher-order procedures

Séminaire, 10 mars 2016

Le matin, nous serons a priori en salle B1 (4ème étage). L'après-midi, nous serons en amphi B (3è étage).

Julien Melleray (Univ. Lyon 1), An introduction to the theory of Borel complexity of classification problems.
Laurent Regnier (Univ. Aix-Marseille), Réalisabilité classique, vers de nouveaux modèles de ZF ?
Pierre Simon (Univ. Lyon 1), Autour des structures NIP et du lemme de régularité de Szemeredi

Séminaire, 11 février 2016

Nous serons en amphi B toute la journée (3è étage, site Monod de l'ENS Lyon).

Thorsten Altenkirch (University of Nottingham (UK)), What is a category? (in univalent type theory)
Simon Boulier (INRIA), Model structure in Homotopy Type Theory
Nicolas Tabareau (INRIA, inventeurs du monde numérique), Enlarge your Coq using Forcing.

Séminaire, 14 janvier 2016

The talks will take place

in salle des thèses (ground floor) in the morning;
in amphi I (not C !!!! -- neither C, nor L) (ground floor, opposite part of the building) in the afternoon.

Raphaëlle Crubillé (Univ. Paris 7 & Univ. Bologna), Metrics Reasoning about lambda-terms
Sam Staton (Oxford University), Algebraic effects, linearity, and quantum programming languages
Lionel Vaux (Univ. Aix-Marseille), A characterization of strong normalizability as a finiteness structure via the Taylor expansion of λ-terms, with applications.

Séminaire, 3 décembre 2015

Jonas Frey (Univ. Copenhagen (talk given in Salle des Thèses, ground floor)), Toposes from Krivine realizability with side effects
Yves Guiraud (INRIA), Théorie de Squier et application aux monoïdes d'Artin
Rodolphe Lepigre (Université de Savoie), A call-by-value realizability model for PML

Séminaire, 5 novembre 2015

Bob Atkey (Strathclyde Univ., UK), Type systems for programming with coinductive data types
Jean-Jacques Lévy (INRIA), The cost of usage in the lambda-calculus
Gabriel Scherer (INRIA), Multi-focusing the lambda-calculus.

Séminaire, 1 octobre 2015

Beniamino Accattoli (INRIA), Proof nets and the lambda-calculus 2.0
Ugo de'Liguoro (Università di Torino), Intersection types for lambda-calculi with control
Thomas Leventis (Institut de Mathématiques de Luminy), Theories in Probabilistic lambda-calculus.

Séminaire, 21 mai 2015

Arthur Charguéraud (Toccata - INRIA), Vérification interactive de programmes impératifs, avec CFML
Étienne Miquey (Laboratoire PPS, Montevideo), Realizability games for the specification problem
Antonino Salibra (Univ. Ca' Foscari, Venezia), Logics via algebras and substitutions

Séminaire, 9 avril 2015

Charles Grellois (Univ. Paris Diderot), Categorical semantics of linear logic and higher-order model-checking
Sylvain Salvati (INRIA, Université de Bordeaux), Model construction for higher-order model-checking
Igor Walukiewicz (CNRS, Labri), Verification of behavioural properties of higher-order programs

Séminaire, 12 mars 2015

Amina Doumane (Université Paris Diderot and ENS Cachan), On the dependencies of logical rules
Thomas Ehrhard (CNRS, Univ. Paris Diderot), Un critère de correction de Christian Rétoré
Giulio Guerrieri (Université Paris Diderot), Injectivity of relational semantics for connected MELL proof-structures via Taylor expansion

Séminaire, 5 février 2015

! The talk by J. Endrullis will be in room B1 (4th floor).

Anupam Das (LIP, ENS Lyon), Theories of bounded arithmetic for deep inference proof systems
Jörg Endrullis (Vrije Universiteit Amsterdam), Clocked lambda-calculus
Andrew Polonski (PPS-LIPN), Toward extensional type theory with decidable type-checking

Séminaire, 4 décembre 2014

Cette réunion se tiendra à Marseille, plus précisément à Luminy (notez au passage les horaires inhabituels).

Pour aller à Luminy, voici un lien, et voici un plan du campus.

Nous serons le matin dans l'amphi 1 du bâtiment A : c'est le rectangle bleu qui porte le numéro 6 sur le plan. Après avoir déjeuné dans une bonne auberge, nous serons l'après-midi dans les locaux du labo I2M, qui se trouve dans la partie CNRS du bâtiment TPR2: c’est le rectangle orange numéro 5.

Guillaume Geoffroy (ENS Paris), Classical realizability models of ZF, ∇2, and the model of threads
Paul Levy (Birmingham University), Transition systems over games
Kazushige Terui (Kyoto University), Some topics on hypersequents

Séminaire, 13 novembre 2014

Dimitri Ara (Univ Aix-Marseille), Street's orientals and Mac Lane's coherence theorem
Lucca Hirschi (ENS Cachan), Partial order reduction for the applied pi-calculus
Jean-Baptiste Jeannin (Carnegie Mellon University), Semantic Foundations for Networks

Séminaire, 16 octobre 2014

Flavien Breuvart (PPS (Paris 7)), De la caractérisation des modèles de H*
Paulin Jacobé de Naurois (CNRS - Univ. Paris 13), Reachability in Vector Addition with States and Split/Join Transitions
Sylvain Schmitz (LSV, ENS Cachan), Complexity in propositional substructural logics and counter systems

Séminaire, 25 septembre 2014

Ugo Dal Lago (Università di Bologna, Italie), Towards a Coinductive Characterization of Computational Indistinguishability
Ulrich Schöpp (LMU, Munich), On the Relation of Interaction Semantics to Continuations and Defunctionalization
Valeria Vignudelli (Università di Bologna), On the Discriminating Power of Higher-order Languages

Séminaire, 3 avril 2014

Emmanouel Beffara (Université d'Aix-Marseille), A logical view on scheduling in concurrency
Giovanni Bernardi (Univ. Lisboa (Portugal)), Mutually testing processes
Fanny He (University of Bath (UK)), A characterization of the Taylor Expansion of λ-terms

Séminaire, 13 mars 2014

Hugo Férée (LORIA), A game semantics approach to complexity
Pierre-Marie Pédrot (PPS, Univ. Paris 7), Can Dialectica break bricks?
Benoît Valiron (PPS, Univ. Paris 7), Towards a formal analysis of quantum algorithms

Séminaire, 13 février 2014

Gilles Barthe (IMDEA (Madrid)), Verified implementations of cryptographic standards
Giuseppe Castagna (CNRS - Univ. Paris Diderot (Paris 7)), Polymorphic Functions with Set-Theoretic Types
Luke Ong (Oxford University), Functions, Concurrency and Automatic Verification

Séminaire, 12 décembre 2013

This meeting will take place in Paris, Amphithéâtre 9E, Université Denis Diderot (Paris 7), esplanade Pierre Vidal-Naquet 75013 Paris (Metro Bibliothèque François Mitterrand, reachable by line 14 from Gare de Lyon).

Hyeonseung Im (LRI (Orsay)), A modal logic internalizing normal proofs
Guy McCusker (University of Bath), Weighted relational models of typed lambda-calculi
Vincent Padovani (PPS - Paris 7), Ticket entailment is decidable

Séminaire, 14 novembre 2013

Beniamino Accattoli (Univ. di Bologna), Toward a New Theory of Exponential Proof-Nets
Dominic Hughes (Stanford), Is linear logic two-thirds wrong (for classical first-order logic)?
Neelakantan R. Krishnaswami (Max Planck Institute), Types for Higher-Order Functional Reactive Programming

Séminaire, 17 octobre 2013

Aloïs Brunel (Univ. Paris 13), Composing forcing and classical realizability: the monitoring calculus
Guillaume Brunerie (Univ. Nice Sophia Antipolis), Homotopy type theory and homotopy groups of spheres
Matteo Mio (CWI, Amsterdam), Semantic Foundations of Quantitative (real-valued) Logics based on Functional Analysis

Séminaire, 26 septembre 2013

Michele Basaldella, An interactive semantics for classical proofs
Michele Pagani (LIPN, Univ. Paris 13), Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF
Christophe Raffalli (LAMA, Université de Savoie), Nullstellensatz and Positivestellensatz from cut-elimination

Séminaire, 16 mai 2013

Jean-Marie Madiot (ENS Lyon), A pi-calculus with preorders
Andrzej Murawski (University of Warwick), Deconstructing general references via game semantics
Alexandra Silva (Radboud University Nijmegen), Coalgebra: applications in automata theory and programming language design

Réunion ANR Récré, 11 avril 2013

Guillaume Munch-Maccagnoni (Univ. Paris 7), When composition is not associative
Colin Riba (ENS Lyon), Forcing MSO on Infinite Words in Weak MSO
Nicolas Tabareau (INRIA, Inventeurs du monde numérique), Univalence for free, not yet ...

Séminaire, 14 mars 2013

Emmanuel Beffara (Université d'Aix-Marseille), Proofs as schedules
Robin Cockett (University of Calgary), Linear types as a semantics for concurrency: passing messages and defining protocols
Chung-Kil Hur (Microsoft Research Cambridge), The Power of Parameterization in Coinductive Proof

Rencontre annuelle GeoCal, 15 février 2013

Rencontre annuelle du groupe de travail <a href="http://iml.univ-mrs.fr/~regnier/gdr-im/">Géométrie du Calcul (GeoCal)</a> du <a href="http://www.gdr-im.fr/">GDR Informatique Mathématique</a>

Flavien Breuvart (Université Paris Diderot), Une bien étrange caractérisation de l'adéquation complète dans les domaines de Scott
Pierre-Louis Curien (CNRS), Revisiting the categorical interpretation of dependent type theory
Yves Lafont (Université d'Aix-Marseille) et Pierre Rannou (Université d'Aix-Marseille), Réécriture de diagrammes convergente pour l'algèbre linéaire
Paul-André Melliès (CNRS), Logique tensorielle et principe de chiralité
Jean-Baptiste Midez (Université d'Aix-Marseille), Quelques aspects combinatoires du lambda-calcul avec ressources
Thomas Seiller (INRIA), Espace Logarithmique et Permutations

Séminaire, 14 février 2013

Cette journée Chocola sera suivie d'une rencontre du Groupe de travail Geocal du GDR IM, le 15 février.

Giulio Manzonetto (Université Paris-Nord), Loader and Urzyczyn are Logically Related
Guilhem Moulin (Chalmers, Sweden), Type Theory in Colors
Antonino Salibra (Università Cà Foscari, Venezia, Italy), From Lambda Calculi to Universal Algebra and Topology: Back and Forth

Séminaire, 17 janvier 2013

Alastair F. Donaldson (Imperial College, London), GPUVerify: a Verifier for GPU Kernels
Michele Pagani (Univ. Paris 13), Syntax vs Semantics: a quantitative bridge
Barbara Petit (Inria Rhône-Alpes), Geometry of types

Séminaire, 6 décembre 2012

Attention cette rencontre aura lieu à Paris.

Gérard Boudol (INRIA), Relaxed Semantics of Concurrent Programs
Matthew Hennessy (Trinity College, Dublin), A theory of communicating transactions
Antoine Madet, Complexité Implicite de Lambda-Calculs Concurrents (soutenance de thèse)

Réunion ANR Récré, 15 novembre 2012

Réunion du projet ANR Récré ouverte à tous les participants des rencontres CHoCoLa.

Séminaire, 11 octobre 2012

Christophe Raffalli (LAMA - Université de Savoie), Realisability, call-by-value and Ramsey theorem
Thomas Seiller (LAMA - Université de Savoie), Interaction Graphs
Bernardo Toninho (Carnegie Mellon University), Linear Logic: A logical foundation for concurrent computation

Séminaire, 10 mai 2012

Marcelo Fiore (University of Cambridge), Lie in Logic
Samuel Mimram (MeASI, CEA Saclay), The higher-dimensional structure of posets
Paulo Oliva (Queen Mary University of London), Some Connections Between Proof Theory and Game Theory

Séminaire, 5 avril 2012

Gabriel Kerneis (PPS, Université Paris Diderot), From threads to events through classical program transformations
Alexandre Miquel (ENS Lyon), Classical realizability models, parallel-or and Boolean valued models
Francesco Zappa Nardelli (Moscova, INRIA Paris-Rocquencourt), Verifying Fence Elimination Optimisations

Séminaire, 15 mars 2012

Nicolas Guenot (LIX/Ecole Polytechnique & PPS/Univ. Paris Diderot), Nested typing and communication in the lambda-calculus
Dale Miller (INRIA Saclay & LIX/Ecole Polytechnique), Proof certificates as focused sequent proofs
Jean-Bernard Stefani (Sardes - INRIA Rhone-Alpes), Reversing (HO)pi

Inauguration Récré, 12 janvier 2012

Journée inaugurale du projet ANR Récré.

Olivier Coucharière (Chargé de mission à l'ANR), Présentation ANR
Hugo Herbelin (PPS/PiR2 - Université Paris Diderot), Proving with side-effects
Guilhem Jaber (École des Mines de Nantes), Forcing the Calculus of Constructions to get generalized inductive types
Thomas Streicher (TU Darmstadt), A categorical approach to Krivine's classical realizability

Séminaire, 8 décembre 2011

Alexis Bernardet (LIX-ENS Cachan), A simple presentation of the effective topos
Jean-Christophe Filliâtre (LRI - Université Paris Sud), Deductive Program Verification with Why3
Damien Pous (Sardes - Grenoble), Hopcroft, Karp, and up-to techniques

Séminaire, 10 novembre 2011

Thibaut Balabonski (PPS - Université Paris Diderot), Le λ-lifting vu comme un événement silencieux
Stefan Hetzl (PPS - Univsersité Paris Diderot), Cut-Elimination and Cut-Introduction
Daniele Varacca (PPS - Université Paris Diderot), Parallel extrusion in the π-calculus, or the limits of stability

Séminaire, 13 octobre 2011

Thomas Braibant (INRIA Grenoble), De coquets circuits
Agathe Chollet (IML, Marseille) et Laurent Fuchs (XLIM-SIC, Poitiers), Autour de la droite d'Harthong-Reeb
Lorenzo Tortora de Falco (Rome 3), Weak normalization, strong normalization and confluence of Linear Logic proof-nets: the semantic point of view

Rencontre, 26 juin 2025

Rencontre, 15 mai 2025

Rencontre, 3 avril 2025

Rencontre, 13 mars 2025

Rencontre, 6 février 2025

Rencontre, 21 novembre 2024

Rencontre, 17 octobre 2024

Rencontre, 19 septembre 2024

Rencontre, 27 juin 2024

Rencontre, 23 mai 2024

Rencontre, 4 avril 2024

Rencontre, 14 mars 2024

Rencontre, 25 janvier 2024

Rencontre, 14 décembre 2023

Rencontre, 16 novembre 2023

Rencontre, 19 octobre 2023

Rencontre, 28 septembre 2023

Rencontre, 15 juin 2023

Rencontre, 11 mai 2023

Séminaire, 30 mars 2023

[Rencontre] The event is canceled, 9 mars 2023