FLoC on Friday, July 9th

See also the by session program.

Coq	DCM	DTP	ITRS	IWS	LOLA	MLQA	PCARC	PPC
09:00‑09:30 Sean Wilson, Jacques Fleuriot and Alan Smaill Inductive Proof Automation for Coq 09:30‑10:00 Chung-Kil Hur Heq: A Coq library for Heterogeneous Equality	09:00‑10:00 Gordon Plotkin (University of Edinburgh) Hierarchical Petri Nets	09:00‑10:00 Ana Bove (Chalmers University) 10 Years of Partiality and General Recursion	09:00‑10:00 Adriana Compagnoni (Stevens Inst. of Technology) Relating Church-style and Curry-style Subtyping	09:00‑10:00 Dan Dougherty (Worcester Polytechnic Institute, USA) Game Strategies and Rule-Based Systems	08:50‑09:00 Opening 09:00‑10:00 Gerard Berry (INRIA, College de France) What could be the right balance between abstract and fine-grain computational properties?	09:00‑09:30 Bernhard Steffen From the How to the What: Static Analysis via Model Checking 09:30‑10:00 Flemming Nielson Model Checking is Static Analysis of Modal Logic	09:00‑10:00 Andrej Bauer (Ljubljana) Reflexive domains and coherence numbers
10:00‑10:30 Coffee break
11:00‑11:30 Jean-francois Monin Proof Trick: Small Inversions 11:30‑12:00 anne mulhern Strengthening the inversion Tactic in Coq 12:00‑12:30 Keiko Nakata and Tarmo Uustalu Mixed induction-coinduction at work for Coq 12:30‑13:00 Paolo Herms Certification of a chain for deductive program verification	10:30‑11:00 Luca Cardelli Two-Domain DNA Strand Displacement 11:00‑11:30 Miklos Bartha Turing automata and graph machines 11:30‑12:00 James Cheney Causality and the Semantics of Provenance 12:00‑12:30 A. Steven Younger and Emmett Redd Computing by Means of Physics-Based Optical Neural Networks	10:30‑11:00 Andreas Abel (University of Munich) Parametric Dependent Function Types 11:00‑11:30 Edwin Brady (University of St Andrews) Practical, efficient programming with dependent types 11:30‑12:00 Anton Setzer (University of Swansea) Coalgebras in dependent type theory 12:00‑12:30 Nils Anders Danielsson (University of Nottingham) Operational Semantics Using the Partiality Monad	10:30‑11:00 Luca Padovani Session Types = Intersection Types + Union Types 11:00‑11:30 Elena Giachino On Semantic Subtyping and Safe Object-Oriented Sessions 11:30‑12:00 Joshua Dunfield Untangling Typechecking of Intersections and Unions 12:00‑12:30 Vilhelm Sjöberg and Aaron Stump Equality, Quasi-Implicit Products, and Large Eliminations	10:30‑11:00 Alvaro Garcia, Pablo Nogueira and Emilio Jesus Gallego Arias The Beta Cube 11:00‑11:30 Alex Gerdes, Bastiaan Heeren and Johan Jeuring Properties of Exercise Strategies 11:30‑12:00 Bernhard Gramlich and Felix Schernhammer Termination of Rewriting with - and Automated Synthesis of - Forbidden Patterns 12:00‑12:30 Olivier Namet and Maribel Fernández A strategy language for graph rewriting systems	10:30‑11:30 Dan Ghica (University of Birmingham) Geometry of Synthesis: Semantics-directed hardware compilation 11:30‑12:00 Magnus O. Myreen and Michael J. C. Gordon Machine code: architecture-independent formal verification and proof-producing compilation 12:00‑12:30 Ugo Dal Lago On the Role of Interaction in Implicit Computational Complexity	10:30‑11:00 Marta Kwiatkowska Quantitative Abstraction Refinement 11:00‑11:30 Joost-Pieter Katoen Invariant Generation for Probabilistic Programs 11:30‑12:00 Marsha Chechik / Arie Gurfinkel Partial Models and Software Model-Checking 12:00‑12:30 Orna Grumberg The 2-Valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking.	10:30‑11:30 Jaap van Oosten (Utrecht) Some more on relative realizability 11:30‑12:30 Pino Rosolini (Genova) Remarks on realizability
12:30‑14:00 Lunch
14:00‑14:30 Hugo Herbelin to be anounced 14:30‑15:00 Thomas Braibant and Damien Pous Rewriting Modulo Associativity and Commutativity	14:00‑15:00 Russ Harmer (CNRS, Paris) Rule-based Modeling: Theory and Practice	14:00‑14:30 Darin Morrison (University of Nottingham) Mechanizing Metatheory via Dependently Typed Programming 14:30‑15:00 Antonis Stampoulis (Yale University) VeriML: Type-safe computation of logical terms inside a language with effects	14:00‑15:00 Simona Ronchi Della Rocca (Univ. of Torino) Intersection and Union Logic	14:00‑15:00 Assia Mahboubi (INRIA, France) Organizing and using algebraic structures in large developments of formalized mathematics	14:00‑15:00 Alex Simpson (LFCS, University of Edinburgh) Linear types for continuations	14:00‑14:30 David Monniaux Policy Iteration for Static Analysis 14:30‑15:00 Michael Huth From Validating Quantitative Models to Generating Valid Ones	14:00‑15:00 John Longley (Edinburgh) In what 2-category do PCAs most naturally live?	14:00‑15:00 Nicola Galesi (Universita di Roma) The Complexity of Proofs in Parameterized Resolution
15:00‑15:30 Coffee break
15:30‑16:00 Bas Spitters and Eelis van der Weegen Developing the algebraic hierarchy with type classes in Coq 16:00‑16:30 Vladimir Komendantsky, Alexander Konovalov and Steve Linton Experience of interfacing Coq+SSReflect and GAP 16:30‑17:00 Yves Bertot and Assia Mahboubi Root isolation for one-variable polynomials	15:30‑16:00 Vincent Danos and Nicolas Oury Equilibrium and Termination 16:00‑16:30 Damian Markham, Janet Anders, Michal Hajdusek and Vlatko Vedral Measurement Based Quantum Computation on Fractal Lattices 16:30‑17:00 Janet Anders and Elisabeth Rieper Continuous variable entanglement in biological systems 17:00‑17:30 Benoît Valiron Semantics of a Typed Algebraic Lambda-calculus 17:30‑18:00 German Terrazas, Dario Landa-Silva and Krasnogor Natalio Towards the Design of Heuristics by means of Self-Assembly	15:30‑16:00 Carsten Schuermann (IT University Copenhagen) The HOL-Nuprl connection in Delphin 16:00‑16:30 Brigitte Pientka (McGill University) Type reconstruction in dependently typed programming 16:30‑17:00 Dan Licata (Carnegie Mellon University) Security-Typed Programming within Dependently Typed Programming	15:30‑16:00 Steffen van Bakel Sound and Complete Typing for Lambda-Mu 16:00‑16:30 Paola Giannini, Mariangiola Dezani-Ciancaglini and Elena Zucca Intersection types for unbind and rebind (Extended Abstract)	15:30‑16:00 René Thiemann, Jürgen Giesl, Peter Schneider-Kamp and Christian Sternagel Loops under Strategies ... Continued 16:00‑16:20 Pascal Fradet, Jean-Louis Giavitto and Marnes Hoff Refinement of Chemical Programs using Strategies 16:20‑16:40 Ian Mackie Closed cut-elimination in linear logic 16:40‑17:00 Detlef PLUMP Graph Programs	15:30‑15:50 Nick Benton and Chung-kil Hur Step-Indexing: The Good, the Bad and the Ugly 15:50‑16:10 Guilhem Jaber and Nicolas Tabareau Krivine realizability for compiler correctness 16:10‑16:30 Shin-ya Katsumata and Rasmus Møgelberg Fullness of monadic translation by TT-lifting 16:30‑17:00 Panel Discussion 17:00‑17:20 Rasmus Ejlers Møgelberg and Sam Staton Full abstraction in a metalanguage for state 17:20‑17:40 Antoine Madet, Roberto M. Amadio and Patrick Baillot An Affine-Intuitionistic System of Types and Effects: Confluence and Termination 17:40‑18:00 Nathaniel Charlton and Bernhard Reus A deeper understanding of the deep frame axiom (extended abstract)	15:30‑17:00 MLQA Business Meeting (open to all attendees) about the future of MLQA and future research collaborations	15:30‑16:30 Thomas Streicher (Darmstadt) A categorical account of Krivine's classical realizability	15:30‑16:00 Eli Ben-Sasson and Jakob Nordström Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions 16:00‑16:30 Stefan Dantchev Parameterized Proof Complexity 17:00‑17:30 Uwe Bubeck, Hans Kleine Büning, Anja Remshagen and Xishun Zhao Expressiveness and Complexity of Subclasses of Quantified Boolean Formulas 17:30‑18:00 Olga Tveretina Ordered Binary Decision Diagrams Do Not Simulate Resolution Polynomially