P R O G R A M 

Full Program Workshop please see below

Note: In the program below you can click on a title to view the abstract and download the specific paper

Monday 24 June, 2019 - Workshop

Venue: Technical University of Dortmund ONLY on 24/06

WPTE 2019 UNIF 2019
08:00 Registration
09:00 - 10:00 Session 1
Chair:Vivek Nigam
Session 1
Chair: Daniele Nantes
Invited Talk: External Termination Proofs for Isabelle/HOL
Rene Thiemann, University of Innsbruck
Invited Talk: Rethinking Unification Theory
Jörg Siekmann
10:00 - 10:30 Coffee Break
10:30 - 11:30 Session 2
Chair: David Sabel
Session 2
Chair: TBD
10:30 - 11:00 Space Improvements for Total Garbage Collection
Manfred Schmidt-Schauss and Nils Dallmeyer
Unification of Multisets with Multiple Labelled Multiset Variables
Zan Naeem and Giselle Reis
11:00 - 11:30 On Determinization of Inverted Grammar Programs via Context-Free
Naoki Nishida and Minami Niwa
Formalising Nominal AC-Unification
Mauricio Ayala-Rincón, Maribel Fernández and Gabriel Ferreira Silva
11:30 - 12:30 Session 3
Chair: TBD
Parameters for Associative and Commutative Matching
Luis Bustamante, Ana Teresa Martins and Francicleber Ferreira
Invited Talk: Strategic Graph Rewriting is an Interactive Modelling Framework
Maribel Fernandez, King's College London

12:00 - 12:30

On Forward-closed and Sequentially-closed String Rewriting Systems
Yu Zhang, Paliath Narendran and Heli Patel
12:30 - 14:00 Lunch Break
14:00 - 15:30 Session 4
Chair: Naoki Nishida
Session 3
Chair: TBD
Invited Talk: SQL for combinatori,al optimization problems and SMT - based solving by SQL transformation
Masahiko Sakai, Nagoya University

14:00 - 14:30

Nominal Unification with Letrec and Environment-Variables
Manfred Schmidt-Schauss and Yunus David Kerem Kutz

14:30 - 15:00

On Asymmetric Unification for the Theory of XOR with a Homomorphism
Christopher Lynch, Andrew M Marshall, Catherine Meadows, Paliath Narendran and Veena Ravishankar

15:00 - 15:30

A Coq Formalization of Boolean Unification
Daniel Dougherty
15:30 - 16:00 Coffee Break
16:00 - 17:00 Session 5
Chair: TBD
Session 4
Chair: TBD
16:00 - 16:30 Formalisation of Normalisation of the Simply Typed Lambda Calculus in F*
Sebastian Sturm
Invited Talk: Maude strategies for narrowing
Narciso Martí-Oliet
16:30 - 17:00 On Formalizing a Transformation of IMP Programs into Logically Constrained Term Rewriting Systems in Isabelle/HOL
Ryota Nakayama and Naoki Nishida

17:00 - 17:30

Solving Proximity Constraints
Temur Kutsia and Cleo Pau

17:30

Asymmetric Unification and Disunification for the theory of Abelian groups with a homomorphism(AGh) Veena Ravishankar, Paliath Narendran and Kimberly Cornell

Tuesday 25 June

08:00 Registration and opening
09:00
-
10:00

FSCD Invited Talk
Chair: Dan Dougherty

Beniamino Accattoli

A Fresh Look at the lambda-Calculus

10:00
-
10:30
Coffee Break
10:30
-
12:30

FSCD Theme: Lambda calculus
Chair: Ugo De'Liguoro

Maciej Bendkowski
Towards the average-case analysis of substitution resolution in lambda-calculus
Pierre Vial
Sequence Types for Hereditary Permutators
Ugo Dal Lago and Thomas Leventis
On the Taylor Expansion of Probabilistic lambda-terms
Simona Kašterović and Michele Pagani
The Discriminating Power of the Let-in Operator1in the Lazy Call-by-Name Probabilistic lambda-Calculus
12:30
-
14:00
Lunch Break
14:00
-
15:30
FSCD Theme: Calling Paradigms
Chair: Paweł Urzyczyn
José Espírito Santo, Luís Pinto, and Tarmo Uustalu
Modal embeddings and calling paradigms

Małgorzata Biernacka and Witold Charatonik
Deriving an Abstract Machine for Strong Call by Need

Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski
Typed Equivalence of Effect Handlers and Delimited Control

15:30
-
16:00
Coffee Break
16:00
-
17:30
FSCD Theme: Logic and models of computation
Chair: Mauricio Ayala Rincon
Alejandro Díaz-Caro and Gilles Dowek
Proof Normalisation in a Logic Identifying Isomorphic Propositions
Dominique Larchey-Wendling and Yannick Forster
Hilbert’s Tenth Problem in Coq
Paulin Jacobé de Naurois
Pointers in Recursion: Exploring the Tropics
19:00 Reception

Wednesday 26 June

Main Conference IFIP 2019
08:00 Registration
09:00
-
10:00

FSCD Invited Talk
Chair: José Espírito Santo

08:30 - 9:00

Welcome
Coffee Break
Amy P. Felty

A Linear Logical Framework in Hybrid

Session 1
Cynthia Kop
Cons - Free Rewriting
10:00
-
10:30
Coffee Break
10:30
-
12:30

FSCD Theme: Types
Chair: Thomas Ehrhard

Session 2
Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto
lambda!-calculus, Intersection Types, and Involutions

10:30 - 11:30

Rene Thiemann
Improved Certification of Complexity Proofs for Term Rewrite System
Luigi Liquori and Claude Stolze
The Delta-calculus: Syntax and Types

11:30 - 11:45

Herman Geuvers
Informal Report on FSCD
Niccolò Veltri and Niels van der Weide
Guarded Recursion in Agda via Sized Types

11:45 - 12:30

Report on IFIP
Ambrus Kaposi, Simon Huber, and Christian Sattler
Gluing for type theory
12:30
-
14:00
Lunch Break
14:00
-
15:30
FSCD Theme: Homotopy Type Theory
Chair: Herman Geuvers
Session 3
Thierry Coquand, Simon Huber, and Christian Sattler
Homotopy canonicity for cubical type theory

14:00 - 15:00

Silvia Ghilezan
Denotational and Operational Preciseness of Subtyping

Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer
Cubical Syntax for Reflection-Free Extensional Equality

Report ISR

Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide
Bicategories in Univalent Foundations

15:30
-
16:00
Coffee Break
16:00
-
17:30
FSCD Theme: Semantics
Chair: Thierry Coquand
Business Meeting
Clovis Eberhart, Tom Hirschowitz, and Alexis Laouar
Template games, simple games, and Day convolution
Thomas Ehrhard
Differentials and distances in probabilistic coherence spaces
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi
Modular specification of monads through higher-order presentations

Thursday 27 June

08:00 Registration
09:00
-
10:00

FSCD Invited Talk
Chair: Cynthia Kop

  Hongseok Yang

Some semantic issues in probabilistic programming languages

10:00
-
10:30
Coffee Break
10:30
-
12:30

FSCD Theme: Rewriting
Chair: Aart Middeldorp

Mirai Ikebuchi
A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods
Alfons Geser, Dieter Hofbauer, and Johannes Waldmann
Sparse Tiling through Overlap Closures for Termination of String Rewriting
David M. Cerna and Temur Kutsia
A generic framework for higher-order generalizations
Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, and Alberto Verdejo
Model checking strategy-controlled rewriting systems
(System Description)
12:30
-
14:00
Lunch Break
14:00
-
15:00
FSCD Theme: Rewriting and Types
Chair: Johannes Waldmann

Łukasz Czajka and Cynthia Kop
Polymorphic Higher-order Termination

Frédéric Blanqui, Guillaume Genestier and Olivier Hermant
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

15:00
-
15:30
Group Photo
17:00
-
22:30
Excursion & Banquet

Friday 28 June

Main Conference IWC 2019 / HOR 2019
08:00 Registration
09:00
-
10:00

FSCD Invited Talk
Chair: Temur Kutsia

Session 1
Chair: Mauricio Ayala-Rincón

09:00 - 09:15

Welcome
Sarah Winkler

Extending Maximal Completion

Invited Talk: Higher-order Termination
Cynthia Kop
10:00
-
10:30
Coffee Break
10:30
-
11:00

FSCD Theme: Rewriting
Chair: Delia Kesner

Session 2
Chair: Stefano Guerrini
Claudia Faggian
Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms
RP IWC: Proving Non-Joinability using Weakly Monotone Algebras
Bertram Felgenhauer and Johannes Waldmann
11:00
-
12:30
FSCD Theme: Linear Logic
Chair: Stefano Guerrini

11:00 - 11:30

RP IWC: The Diamond Lemma for non-terminating rewriting systems using deterministic reduction strategies
Cyrille Chenavier and Maxime Lucas

Ross Horne
The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic

11:30 - 12:00

RP IWC: infChecker, a tool for checking infeasibility
Raúl Gutiérrez and Salvador Lucas
Yosuke Fukuda and Akira Yoshimizu
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4

12:00 - 12:30

RP HOR: SizeChangeTool: A Termination Checker for Higher-Order Rewriting with Dependent Types
Guillaume Genestier

Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger
Proof nets for first-order additive linear logic

12:30
-
14:00
Lunch Break
14:00
-
14:45
FSCD General Meeting Session 3
Chair: Silvia Ghilezan
Invited Talk: Higher-Order Complexity Analysis With First-Order Tools
Martin Avanzini
14:45 - 15:30 Invited Talk: On the Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms: Maude's Church-Rosser Checker
Francisco Durán
15:30 - 16:00 Coffee Break
16:00 - 16:45 Session 4
Chair: Jakob Grue Simonsen
Invited Talk: On the Clocked Lambda-Calculus
Jörg Endrullis
16:45 - 17:30 Invited Talk: Degrees of extensionality in the theory of Böhm trees
Giulio Manzonetto
17:30 - 18:00 RP IWC: Residuals Revisited
Christina Kohl and Aart Middeldorp
18:00-18:30 CoCo report
Aart Middeldorp

Saturday 29 June, 2019

TLLA 2019 SD 2019
08:00 Registration
09:00 - 10:00 Joint invited talk: Reasoning about languages with control operators
Delia Kesner
10:00 - 10:30 Coffee Break
10:30 - 11:00 Proof nets for non-wellfounded proofs
Abhishek De and Alexis Saurin
Invited Talk: Can we Prove Privacy Properties using the Calculus of Structures
Ross Horne
11:00 - 11:30 A Quantitative Semantics of Differential Linear Logic with Setoids
Zeinab Galal
11:30 - 12:00 Deep inference for proof search
Ozan Kahramanogullari
12:00 - 12:30 Additive to Classical Proof Search
Adam Lassiter
12:30 - 14:00 Lunch Break
14:00 - 15:00 Invited Talk: Call-by-push-value and linear logic: various connections
Paul Blain Levy
Invited Talk: Deciding ATL* satisfiability by tableaux
Serenella Cerrito
15:00 - 15:30 On the expressivity of linear recursion schemes
Pierre Clairambault and Andrzej Murawski
Two deductive systems for the constructive logic S4, a formal verification
Lourdes Del Carmen González Huesca
15:30 - 16:00 Coffee Break
16:00 - 16:30   What are combinatorial proofs?
Lutz Strassburger
16:30 - 17:00 Business Meeting Expansion tree proofs with unification
Michelangelo Mecozzi
17:00 - 17:30 The Jacobson Radical of a Propositional Theory
Peter Schuster

Sunday 30 June, 2019

TLLA 2019 SD 2019
08:00 Registration
09:00 - 10:00 Joint Invited Talk: Semantics and complexity lower bounds
Thomas Seiller
10:00 - 10:30 Coffee Break
10:30 - 11:00 About the Power of Taylor Expansion
Davide Barbarossa and Giulio Manzonetto
Invited Talk: A story of multiplicatives and additives
Andrea Aler Tubella
11:00 - 11:30 What is the Taylor expansion a natural transformation of?
Luc Pellissier
11:30 - 12:00 Standardization via Linear Logic for Call-by-Name, Call-by-Value and Choice Effects
Claudia Faggian and Giulio Guerrieri
A Subatomic Proof System for Binary Decision Trees
Chris Barrett
12:00 - 12:30 The Geometry of Abstract Machines
Beniamino Accattoli, Ugo Dal Lago and Gabriele Vanoni
A graph theoretic extension of Boolean logic
Tim Waring
12:30 - 14:00 Lunch Break
14:00 - 15:00 Invited Talk: Stable Semantics of Probabilistic Higher-Order Programs
Raphaëlle Crubillé.
Invited Talk: Structural proof theory: shedding structure
Revantha Ramanayake
15:00 - 15:30 Transductions in affine logic
Lê Thành Dung Nguyen
Complexity of Reasoning in Residuated Kleene Algebras
Stepan Kuznetsov
15:30 - 16:00 Coffee Break
16:00 - 16:30 The Spinal Atomic Lambda Calculus
David Sherratt
16:30 - 17:00 Kreisel's Conjecture and Reflexion Principles: Two Restricted Versions of the Conjecture
Paulo Guiherme Santos
17:00 - 17:30 On sequent calculi proofs in relevant logics
Mirjana Ilic