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
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:30Yu Zhang, Paliath Narendran and Heli Patel |
|
12:30 - 14:00 | Lunch Break | |
14:00 - 15:30 | Session 4 Chair: Naoki Nishida |
Session 3 |
Invited Talk: SQL for combinatori,al optimization problems and SMT - based solving by SQL transformation Masahiko Sakai, Nagoya University |
14:00 - 14:30Nominal Unification with Letrec and Environment-VariablesManfred Schmidt-Schauss and Yunus David Kerem Kutz |
|
14:30 - 15:00Christopher Lynch, Andrew M Marshall, Catherine Meadows, Paliath Narendran and Veena Ravishankar 15:00 - 15:30Daniel 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:30Temur Kutsia and Cleo Pau 17:30 |
Tuesday 25 June
08:00 | Registration and opening | |
09:00 - 10:00 |
FSCD Invited Talk |
|
Beniamino Accattoli |
||
10:00 - 10:30 |
Coffee Break | |
10:30 - 12:30 |
FSCD Theme: Lambda calculus |
|
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 |
||
Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski |
||
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 |
Welcome |
Amy P. Felty |
Session 1 Cynthia Kop Cons - Free Rewriting |
|
10:00 - 10:30 |
Coffee Break | |
10:30 - 12:30 |
FSCD Theme: Types |
Session 2 |
Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto lambda!-calculus, Intersection Types, and Involutions |
10:30 - 11:30Rene ThiemannImproved Certification of Complexity Proofs for Term Rewrite System |
|
Luigi Liquori and Claude Stolze The Delta-calculus: Syntax and Types |
11:30 - 11:45Herman GeuversInformal Report on FSCD |
|
Niccolò Veltri and Niels van der Weide Guarded Recursion in Agda via Sized Types |
11:45 - 12:30Report 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:00Silvia GhilezanDenotational and Operational Preciseness of Subtyping |
|
Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer |
Report ISR | |
Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide |
||
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 |
|
Hongseok Yang |
||
10:00 - 10:30 |
Coffee Break | |
10:30 - 12:30 |
FSCD Theme: Rewriting |
|
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 |
||
Frédéric Blanqui, Guillaume Genestier and Olivier Hermant |
||
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 |
Session 1 Chair: Mauricio Ayala-Rincón 09:00 - 09:15Welcome |
|
Sarah Winkler |
Invited Talk: Higher-order Termination Cynthia Kop |
||
10:00 - 10:30 |
Coffee Break | ||
10:30 - 11:00 |
FSCD Theme: Rewriting |
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:30RP IWC: The Diamond Lemma for non-terminating rewriting systems using deterministic reduction strategiesCyrille Chenavier and Maxime Lucas |
|
Ross Horne |
11:30 - 12:00RP IWC: infChecker, a tool for checking infeasibilityRaúl Gutiérrez and Salvador Lucas |
||
Yosuke Fukuda and Akira Yoshimizu A Linear-logical Reconstruction of Intuitionistic Modal Logic S4 |
12:00 - 12:30RP HOR: SizeChangeTool: A Termination Checker for Higher-Order Rewriting with Dependent TypesGuillaume Genestier |
||
Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger |
|||
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 |