Program | FSCD 2019

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
09:00 - 10:00	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	11:45 - 12:30 Report on IFIP
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	Report ISR
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
09:00 - 10:00	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
10:30 - 11:00	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
14:00 - 14:45		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
16:00 - 16:45		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	Business Meeting	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

Full Program Workshop please see below

Monday 24 June, 2019 - Workshop

12:00 - 12:30

14:00 - 14:30

14:30 - 15:00

15:00 - 15:30

17:00 - 17:30

17:30

Tuesday 25 June

Beniamino Accattoli

Wednesday 26 June

08:30 - 9:00

Amy P. Felty

10:30 - 11:30

11:30 - 11:45

11:45 - 12:30

14:00 - 15:00

Thursday 27 June

Hongseok Yang

Friday 28 June

09:00 - 09:15

Sarah Winkler

11:00 - 11:30

11:30 - 12:00

12:00 - 12:30

Saturday 29 June, 2019

Sunday 30 June, 2019