Workshop Programme
23 June 2016
CL&C
| Chair: Ulrich Kohlenbach 09:00-10:00Coherent Logic: an overview
9:00
CL&C
| Chair: Ulrich Kohlenbach 10:30-10:55Natural Deduction and Curry-Howard for Herbrand Constructive Logics
10:30
CL&C - Analysis and Set Theory Workshop
| Chair: Fernando Ferreira 10:55-12:35The computational content of Nonstandard Analysis
10:55
Proof Mining in Nonlinear Analysis
11:45
The computational content of Zorn's lemma
12:10
CL&C - Continuations Workshop
| Chair: Ugo de Liguoro 14:00-16:40Denotational semantics of the simplified lambda-mu calculus and a new deduction system of classical type theory
14:00
A continuation-passing-style interpretation of simply-typed call-by-need lambda-calculus with control within System F
14:50
A note on strong normalization in classical natural deduction
15:15
CL&C - Witness Extraction Workshop
| Chair: Stefano Berardi 17:10-18:00On the Herbrand content of LK
17:10
WPTE
| Chair: Horatiu Cirstea 10:30-12:30On upper bounds on the Church-Rosser theorem
10:30
Confluence of Conditional Term Rewrite Systems via Transformations
11:00
An Environment for Analyzing Space Optimizations in Call-by-Need Functional Languages
11:30
An extension of proof graphs for disjunctive parameterised Boolean equation systems
12:00
WPTE
| Chair: Santiago Escobar 14:00-16:00Invited talk: The Complexity of Abstract Machines
14:00
Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems
15:00
Reversible Term Rewriting in Practice
15:30
LFMTP - Contributed Papers
10:30-12:30Mechanizing Proofs about Mendler-style Recursion
10:30
A Rewrite System for Proof Constructivization
11:00
The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid
11:30
Implementing HOL in an Higher Order Logic Programming Language
12:00
LFMTP
14:00-15:00The Incredible Proof Machine
14:00
25 June 2016
HOR - Session I
09:00-10:00Higher-Order Cons-Free Interpreters
9:00
The Expressive Power of Coinductive, Rigid Types with Non-Idempotent Intersections.
9:30
HOR - Session II
10:30-12:30Implementation of Explicit Substitutions: from lambda-sigma to the Suspension Calculus.
10:30
Confluence and Strong Normalization for the CPS Target Language.
11:30
Equivalence of System F and lambda-2: A Case Study of Context Morphisms.
11:00
h-bar: a Plank for Higher-Order Attribute Contraction Schemes.
12:00
HOR - Session III
14:00-16:00Toward Analytic Rewriting Theory.
14:00
Reduction by Decomposition.
14:30
The Calculus of Compositions.
15:00
Characterizing Trees for Lambda-mu terms.
15:30
HOR - Session IV
16:30-18:00Running Interaction Nets on Random Access Machines.
16:30
A Rule-Based Procedure for Equivariant Nominal Unification.
17:00
Untyped Confluence in Dependent Type Theories.
17:30
HoTT-UF
10:30-12:30Compact types and ordinals in univalent type theory
10:30
Classifying types
11:00
HoTT-UF
14:00-16:00Homotopy Type Theory in Lean
14:00
Higher inductive types
15:00
HoTT-UF
17:00-17:30Type theory with native homotopy universes
17:00
HDRA
10:30-12:15Coherence for swallowtailators and Frobenius pseudomonoids
10:30
A topological perspective on interacting algebraic theories
11:30
HDRA
14:00-16:00Formal theory of operadic categories and operads (Invited talk)
14:00
Well founded Path Orderings for Drags
15:15
HDRA
16:30-17:15Column presentations of plactic monoids
16:30
LINEARITY - Proofs
| Chair: Iliano Cervesato 10:30-12:30Invited Talk - A proof theory for model checking: an overview
10:30
Surface proofs for non-commutative linear logic
11:30
Proof diagrams for multiplicative linear logic
12:00
LINEARITY - Programming
| Chair: Damiano Mazza 14:00-16:00Linear beta-reduction
14:00
Krivine machine and Taylor expansion in a non-uniform setting
14:30
Design and Implementation of Concurrent C0
15:00
Non-Blocking Concurrent Imperative Programming with Session Types
15:30
LINEARITY - Models/New directions
| Chair: Maribel Fernández 16:30-18:00Linear Exponential Comonads without Symmetry
16:30
Discussion - End of Linearity 2016
17:30
On Godel's Second Incompleteness Theorem for Arithmetic without Contraction
17:00
LSFA
10:30-12:30A Framework for Defining Type Systems (Invited Talk)
10:30
Controlling File Access with Types
11:30
The Polarized Lambda-calculus
12:00
LSFA
14:00-16:00Relational program verification: an overview
14:00
Hybrid and Subexponential Linear Logics
15:00
Projections for infinitary rewriting
15:30
26 June 2016
HDRA
09:00-10:00Circuits, diagrams, (graphical) linear algebra and control theory
9:00
HDRA
10:30-12:15A Cubical Squier's Theorem
10:30
Reduction Operators: Rewriting Properties and Completion
11:30
HDRA
14:00-16:00Open graphs and hypergraphs (Invited talk)
14:00
Ordered and Combinatorial Structures for Higher-Dimensional Rewriting
15:15
HDRA
16:30-17:15Completion method in higher dimensional polygraphs
16:30
HoTT-UF
09:00-10:00Cubical Type Theory: a constructive interpretation of the univalence axiom
9:00
HoTT-UF
10:30-12:30Modelling Cubical TT in Agda
10:30
Fibred fibration categories
11:00
Splitting dictoses
11:30
IFIP WG 1.6
09:00-09:45Welcome
9:00
One context unification problems solvable in polynomial time
09:15
IFIP WG 1.6
10:30-12:30Programming Coinductive Proofs Using Observations
10:30
Report 2015, Announcement 2017, Proposal 2018
11:15
Discussion: ISR as an IFIP event
11:45
IFIP WG 1.6
14:00-15:45Formalisation of Confluence
14:00
Assessment FSCD
14:45
Discussion future of IFIP
15:00
IFIP WG 1.6
16:30-17:30Business meeting
16:30
ITRS
| Chair: Naoki Kobayashi 09:00-10:00Intersection types, quantitative semantics and linear logic
9:00
ITRS - Regular Talks I
| Chair: Jakob Rehof 10:30-12:30Affine Approximations and Intersection Types
10:30
Relational type-checking for MELL proof-structures. Part 1: Multiplicatives
11:00
Intersections and Unions of Session Types
11:30
Retractions in Intersection Types
12:00
ITRS - Invited Talk \& Regular Talks II
| Chair: Mariangiola Dezani-Ciancaglini 14:00-16:00Intersection types for real number computation
14:00
Intersection Types and Counting
15:00
Intersection Types and Probabilistic Lambda Calculi
15:30
ITRS - Regular Talks III
| Chair: Naoki Kobayashi 16:30-17:00Approximation and (Head) Normalisation for lambda-mu using Strict Intersection Types
16:30
UNIF
| Chair: Manfred Schmidt-Schauß 09:00-10:00Automated Symbolic Proofs of Security Protocols
9:00
UNIF - Unification Algorithms
10:30-12:30The Unification Type of ACUI w.r.t. the Unrestricted Instantiation Preorder is not Finitary
10:30
Approximately Solving Set Equations
11:00
Universal freeness and admissibility
11:30
Overlap and Independence in Multiset Comprehension Patterns
12:00
Let's Unify With Scala Pattern Matching!
12:25
UNIF - Unification and algebra
| Chair: Silvio Ghilardi 14:00-16:00Unification in predicate logic
14:00
Notes on Lynch-Morawska Systems
15:00
Lynch-Morawska Systems on Strings
15:30
UNIF - Applications
16:30-17:00Type unification for structural types in Java
16:30
LSFA
10:30-12:30Formalized Meta-Theory of Sequent Calculi for Substructural Logics
10:30
Generalized Refocusing: a Formalization in Coq
11:00
The Descriptive Complexity of Logics with Relational Fixed-Point
11:30
A Formalisation of Nominal alpha-equivalence with A and AC Function Symbols
12:00
LSFA
14:00-16:00Problem Solving with SAT Oracles (Invited Talk)
14:00
Generalized Probabilistic Satisfiability
15:00
From cut-free calculi to automated deduction: the case of bounded contraction
15:30