Workshop Programme


23 June 2016

CL&C

| Chair: Ulrich Kohlenbach 09:00-10:00
Coherent Logic: an overview
9:00
Marc Bezem

CL&C

| Chair: Ulrich Kohlenbach 10:30-10:55
Natural Deduction and Curry-Howard for Herbrand Constructive Logics
10:30
Federico Aschieri

CL&C - Analysis and Set Theory Workshop

| Chair: Fernando Ferreira 10:55-12:35
The computational content of Nonstandard Analysis
10:55
Sam Sanders
Proof Mining in Nonlinear Analysis
11:45
Daniel Koernlein
The computational content of Zorn's lemma
12:10
Thomas Powell

CL&C - Continuations Workshop

| Chair: Ugo de Liguoro 14:00-16:40
Denotational semantics of the simplified lambda-mu calculus and a new deduction system of classical type theory
14:00
Ken Akiba
A continuation-passing-style interpretation of simply-typed call-by-need lambda-calculus with control within System F
14:50
Hugo Herbelin and Étienne Miquey
A note on strong normalization in classical natural deduction
15:15
José Espírito Santo

CL&C - Witness Extraction Workshop

| Chair: Stefano Berardi 17:10-18:00
On the Herbrand content of LK
17:10
Bahareh Afshari, Stefan Hetzl and Graham Leigh

WPTE

| Chair: Horatiu Cirstea 10:30-12:30
On upper bounds on the Church-Rosser theorem
10:30
Ken-EtsuFujita
Confluence of Conditional Term Rewrite Systems via Transformations
11:00
Karl Gmeiner
An Environment for Analyzing Space Optimizations in Call-by-Need Functional Languages
11:30
Nils Dallmeyer, Manfred Schmidt-Schauß
An extension of proof graphs for disjunctive parameterised Boolean equation systems
12:00
Yutaro Nagae, Masahiko Sakai

WPTE

| Chair: Santiago Escobar 14:00-16:00
Invited talk: The Complexity of Abstract Machines
14:00
Beniamino Accattoli
Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems
15:00
Ryota Nakayama, Naoki Nishida, Masahiko Sakai
Reversible Term Rewriting in Practice
15:30
Naoki Nishida, Adrian Palacios, German Vidal

LFMTP - Contributed Papers

10:30-12:30
Mechanizing Proofs about Mendler-style Recursion
10:30
Rohan Jacob-Rao, Andrew Cave, and Brigitte Pientka
A Rewrite System for Proof Constructivization
11:00
Raphaël Cauderlier
The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid
11:30
Chelsea Battell and Amy Felty
Implementing HOL in an Higher Order Logic Programming Language
12:00
Cvetan Dunchev, Claudio Sacerdoti Coen, and Enrico Tassi

LFMTP

14:00-15:00
The Incredible Proof Machine
14:00
Joachim Breitner

25 June 2016

HOR - Session I

09:00-10:00
Higher-Order Cons-Free Interpreters
9:00
Cynthia Kop and Jakob Grue Simonsen
The Expressive Power of Coinductive, Rigid Types with Non-Idempotent Intersections.
9:30
Pierre Vial

HOR - Session II

10:30-12:30
Implementation of Explicit Substitutions: from lambda-sigma to the Suspension Calculus.
10:30
Vincent Archambault-Bouffard and Stefan Monnier
Confluence and Strong Normalization for the CPS Target Language.
11:30
Jonas Frey
Equivalence of System F and lambda-2: A Case Study of Context Morphisms.
11:00
Jonas Kaiser, Tobias Tebbi and Gert Smolka
h-bar: a Plank for Higher-Order Attribute Contraction Schemes.
12:00
Cynthia Kop and Kristoffer Rose

HOR - Session III

14:00-16:00
Toward Analytic Rewriting Theory.
14:00
Andrew Polonsky, Michele Pagani and Benoit Valiron
Reduction by Decomposition.
14:30
James Laird
The Calculus of Compositions.
15:00
Enno Folkerts
Characterizing Trees for Lambda-mu terms.
15:30
Koji Nakazawa

HOR - Session IV

16:30-18:00
Running Interaction Nets on Random Access Machines.
16:30
Stephane Gimenez and Georg Moser
A Rule-Based Procedure for Equivariant Nominal Unification.
17:00
Takahito Aoto and Kentaro Kikuchi
Untyped Confluence in Dependent Type Theories.
17:30
Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud and Jiaxiang Liu

HoTT-UF

10:30-12:30
Compact types and ordinals in univalent type theory
10:30
Escardo
Classifying types
11:00
Rijke*, Buchholtz

HoTT-UF

14:00-16:00
Homotopy Type Theory in Lean
14:00
Van Doorn
Higher inductive types
15:00
Van der Weide*, Geuvers, Basold

HoTT-UF

17:00-17:30
Type theory with native homotopy universes
17:00
Adams*, Polonsky

HDRA

10:30-12:15
Coherence for swallowtailators and Frobenius pseudomonoids
10:30
Jamie Vicary
A topological perspective on interacting algebraic theories
11:30
Amar Hadzihasanovic

HDRA

14:00-16:00
Formal theory of operadic categories and operads (Invited talk)
14:00
Michael Batanin
Well founded Path Orderings for Drags
15:15
Nachum Dershowitz, Jean-Pierre Jouannaud and Jian-Qi Li

HDRA

16:30-17:15
Column presentations of plactic monoids
16:30
Nohra Hage

LINEARITY - Proofs

| Chair: Iliano Cervesato 10:30-12:30
Invited Talk - A proof theory for model checking: an overview
10:30
Dale Miller
Surface proofs for non-commutative linear logic
11:30
Lawrence Dunn and Jamie Vicary
Proof diagrams for multiplicative linear logic
12:00
Matteo Acclavio

LINEARITY - Programming

| Chair: Damiano Mazza 14:00-16:00
Linear beta-reduction
14:00
Stefano Guerrini
Krivine machine and Taylor expansion in a non-uniform setting
14:30
Antoine Allioux
Design and Implementation of Concurrent C0
15:00
Max Willsey, Rokhini Prabhu and Frank Pfenning
Non-Blocking Concurrent Imperative Programming with Session Types
15:30
Miguel Silva, Mario Florido and Frank Pfenning

LINEARITY - Models/New directions

| Chair: Maribel Fernández 16:30-18:00
Linear Exponential Comonads without Symmetry
16:30
Masahito Hasegawa
Discussion - End of Linearity 2016
17:30
All
On Godel's Second Incompleteness Theorem for Arithmetic without Contraction
17:00
Daniyar Shamkanov

LSFA

10:30-12:30
A Framework for Defining Type Systems (Invited Talk)
10:30
Kaustuv Chaudhuri
Controlling File Access with Types
11:30
Rakan Alsowail and Ian Mackie
The Polarized Lambda-calculus
12:00
José Espírito Santo

LSFA

14:00-16:00
Relational program verification: an overview
14:00
Gilles Barthe
Hybrid and Subexponential Linear Logics
15:00
Joelle Despeyroux, Carlos Olarte and Elaine Pimentel
Projections for infinitary rewriting
15:30
Carlos Lombardi, Alejandro Ríos and Roel de Vrijer

26 June 2016

HDRA

09:00-10:00
Circuits, diagrams, (graphical) linear algebra and control theory
9:00
Pawel Sobocinski

HDRA

10:30-12:15
A Cubical Squier's Theorem
10:30
Maxime Lucas
Reduction Operators: Rewriting Properties and Completion
11:30
Cyrille Chenavier

HDRA

14:00-16:00
Open graphs and hypergraphs (Invited talk)
14:00
Joachim Kock
Ordered and Combinatorial Structures for Higher-Dimensional Rewriting
15:15
Lars Hellström

HDRA

16:30-17:15
Completion method in higher dimensional polygraphs
16:30
Clément Alleaume

HoTT-UF

09:00-10:00
Cubical Type Theory: a constructive interpretation of the univalence axiom
9:00
Mörtberg

HoTT-UF

10:30-12:30
Modelling Cubical TT in Agda
10:30
Orton*, Pitts
Fibred fibration categories
11:00
Uemura*
Splitting dictoses
11:30
Hofmann*, Streicher

IFIP WG 1.6

09:00-09:45
Welcome
9:00
Welcome
One context unification problems solvable in polynomial time
09:15
Ashish Tiwari

IFIP WG 1.6

10:30-12:30
Programming Coinductive Proofs Using Observations
10:30
Brigitte Pientka
Report 2015, Announcement 2017, Proposal 2018
11:15
Johannes Waldmann
Discussion: ISR as an IFIP event
11:45
All

IFIP WG 1.6

14:00-15:45
Formalisation of Confluence
14:00
Mauricio Ayala-Rincón
Assessment FSCD
14:45
All
Discussion future of IFIP
15:00
Discussion future of IFIP

IFIP WG 1.6

16:30-17:30
Business meeting
16:30
Business meeting

ITRS

| Chair: Naoki Kobayashi 09:00-10:00
Intersection types, quantitative semantics and linear logic
9:00
Michele Pagani (Université Paris-Diderot)

ITRS - Regular Talks I

| Chair: Jakob Rehof 10:30-12:30
Affine Approximations and Intersection Types
10:30
Damiano Mazza (Université Paris 13)
Relational type-checking for MELL proof-structures. Part 1: Multiplicatives
11:00
Giulio Guerrieri (Aix-Marseille Université/Università Roma Tre), Luc Pellissier (Université Paris 13) and Lorenzo Tortora De Falco (Università Roma Tre)
Intersections and Unions of Session Types
11:30
Cosku Acay and Frank Pfenning (Carnegie Mellon University)
Retractions in Intersection Types
12:00
Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria and Maddalena Zacchi (Università di Torino)

ITRS - Invited Talk \& Regular Talks II

| Chair: Mariangiola Dezani-Ciancaglini 14:00-16:00
Intersection types for real number computation
14:00
Kazushige Terui (Kyoto University)
Intersection Types and Counting
15:00
Paweł Parys (University of Warsaw)
Intersection Types and Probabilistic Lambda Calculi
15:30
Flavien Breuvart (Inria) and Ugo Dal Lago (University of Bologna)

ITRS - Regular Talks III

| Chair: Naoki Kobayashi 16:30-17:00
Approximation and (Head) Normalisation for lambda-mu using Strict Intersection Types
16:30
Steffen van Bakel (Imperial College London)

UNIF

| Chair: Manfred Schmidt-Schauß 09:00-10:00
Automated Symbolic Proofs of Security Protocols
9:00
Ralf Sasse

UNIF - Unification Algorithms

10:30-12:30
The Unification Type of ACUI w.r.t. the Unrestricted Instantiation Preorder is not Finitary
10:30
Franz Baader and Pierre Ludmann
Approximately Solving Set Equations
11:00
Franz Baader, Pavlos Marantidis and Alexander Okhotin
Universal freeness and admissibility
11:30
Michał Stronkowski
Overlap and Independence in Multiset Comprehension Patterns
12:00
Iliano Cervesato and Edmund Soon Lee Lam
Let's Unify With Scala Pattern Matching!
12:25
Edmund Soon Lee Lam and Iliano Cervesato

UNIF - Unification and algebra

| Chair: Silvio Ghilardi 14:00-16:00
Unification in predicate logic
14:00
Wojciech Dzik and Piotr Wojtylak
Notes on Lynch-Morawska Systems
15:00
Daniel S. Hono, Namrata Galatage, Kimberly A. Gero, Paliath Narendran and Ananya Subburathinam
Lynch-Morawska Systems on Strings
15:30
Daniel S. Hono, Paliath Narendran and Rafael Veras

UNIF - Applications

16:30-17:00
Type unification for structural types in Java
16:30
Martin Plümicke

LSFA

10:30-12:30
Formalized Meta-Theory of Sequent Calculi for Substructural Logics
10:30
Kaustuv Chaudhuri, Leonardo Lima and Giselle Reis
Generalized Refocusing: a Formalization in Coq
11:00
Klara Zielinska and Malgorzata Biernacka
The Descriptive Complexity of Logics with Relational Fixed-Point
11:30
Márcia Farias, Ana Teresa Martins and Francicleber Ferreira
A Formalisation of Nominal alpha-equivalence with A and AC Function Symbols
12:00
Mauricio Ayala-Rincon, Washington de Carvalho-Segundo, Maribel Fernández and Daniele Nantes-Sobrinho

LSFA

14:00-16:00
Problem Solving with SAT Oracles (Invited Talk)
14:00
João Marques Silva
Generalized Probabilistic Satisfiability
15:00
Carlos Caleiro, Filipe Casal and Andreia Mordido
From cut-free calculi to automated deduction: the case of bounded contraction
15:30
Agata Ciabattoni, Bjorn Lellmann, Carlos Olarte and Elaine Pimentel