FLoC on Sunday, July 11th

See also the by session program.

ITP	LICS	RTA	SAT
09:00‑09:30 Norbert Schirmer and Ernie Cohen From Total Store Order to Sequential Consistency: A Practical Reduction Theorem 09:30‑10:00 Freek Verbeek and Julien Schmaltz Proof Pearl: A formal proof of Duato's condition for deadlock-free adaptive networks	08:45‑09:00 Opening 09:00‑09:30 Vince Bárány, Georg Gottlob and Martin Otto Querying the Guarded Fragment 09:30‑10:00 Martin Otto Highly Acyclic Groups, Hypergraph Covers and the Guarded Fragment	09:00‑09:30 Patrick Bahr Partial Order Infinitary Term Rewriting and Böhm Trees 09:30‑10:00 Hans Zantema and Matthias Raffelsieper Proving Productivity in Infinite Data Structures	09:00‑10:00 Yehuda Naveh The Big Deal: Applying Constraint Satisfaction Technologies Where it Makes the Difference
10:00‑10:30 Coffee break
10:30‑11:00 Ramana Kumar and Michael Norrish (Nominal) Unification by Recursive Descent with Triangular Substitutions 11:00‑11:30 Jean-François Dufourd and Yves Bertot Formal study of plane Delaunay triangulation 11:30‑12:00 Sylvie Boldo, François Clément, Jean-Christophe Filliatre, Micaela Mayero, Guillaume Melquiond and Pierre Weis Formal Proof of a Wave Equation Resolution Scheme: the Method Error 12:00‑12:30 Anthony Fox and Magnus Myreen A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture	10:30‑11:00 Vincent Siles and Hugo Herbelin Equality is typable in Semi-Full Pure Type Systems 11:00‑11:30 Andrei Popescu, Elsa Gunter and Chris Osborn Strong normalization of System F by HOAS on top of FOAS 11:30‑12:00 James Laird Game Semantics for a Polymorphic Programming Language 12:00‑12:30 Hugo Herbelin An intuitionistic logic that proves Markov's principle	10:30‑11:00 Marc Sylvestre, Irène Durand and Géraud Sénizergues Termination of linear bounded term rewriting systems 11:00‑11:30 Christian Sternagel and René Thiemann Certified Subterm Criterion and Certified Usable Rules 11:30‑12:00 Friedrich Neurauter and Aart Middeldorp Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers 12:00‑12:30 Carsten Otto, Marc Brockschmidt, Christian von Essen and Jürgen Giesl Automated Termination Analysis of Java Bytecode by Term Rewriting	10:30‑11:00 Stephan Kottler SAT Solving with Reference Points 11:00‑11:30 Dave Tompkins and Holger Hoos Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT 11:30‑11:50 Alexander Nadel and Vadim Ryvchin Assignment Stack Shrinking 11:50‑12:10 Matti Järvisalo and Armin Biere Reconstructing Solutions after Blocked Clause Elimination 12:10‑12:30 Ashish Sabharwal, Bart Selman and Lukas Kroc An Empirical Study of Optimal Noise and Runtime Distributions in Local Search
12:30‑14:00 Lunch
14:00‑14:30 David Harel (Weizmann Institute of Science) Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's. 14:30‑15:00 Gordon Plotkin (University of Edinburgh) Robin Milner, a Craftsman of Tools for the Mind.
15:00‑15:30 Coffee break
15:30‑16:00 Brian Huffman and Christian Urban Proof Pearl: A New Foundation for Nominal Isabelle 16:00‑16:30 John Cowles and Ruben Gamboa Using a First Order Logic to Verify That Some Set of Reals Has No Lebesgue Measure 16:30‑17:00 Tarek Mhamdi, Osman Hasan and Sofiene Tahar On the Formalization of the Lebesgue Integration Theory in HOL	15:30‑16:00 Mark Jenkins, Joel Ouaknine, Alexander Rabinovich and James Worrell Alternating Timed Automata over Bounded Time 16:00‑16:30 Thomas Colcombet and Christof Loeding Regular cost functions over finite trees 16:30‑17:00 Eryk Kopczynski and Anthony Widjaja To Parikh Images of Grammars: Complexity and Applications 17:15‑17:45 Manuel Bodirsky, Martin Hils and Barnaby Martin On the Scope of the Universal-Algebraic Approach to Constraint Satisfaction 17:45‑18:15 Marcin Kozik and Libor Barto New conditions for Taylor varieties and CSP	15:30‑16:00 Alexander Koller and Stefan Thater Underspecified computation of normal forms 16:00‑16:30 Karl Gmeiner, Bernhard Gramlich and Felix Schernhammer On (Un)Soundness of Unravelings 16:30‑17:00 Adrian Riesco, Alberto Verdejo and Narciso Marti-Oliet Declarative Debugging of Missing Answers for Maude Specifications 17:00‑17:20 Mark Hills and Grigore Rosu A Rewriting Logic Semantics Approach to Modular Program Analysis	15:30‑16:00 Kazuhisa Makino, Suguru Tamaki and Masaki Yamamoto An Exact Algorithm for the Boolean Connectivity Problem for k-CNF 16:00‑16:30 Hadi Katebi, Karem Sakallah and Igor Markov Symmetry and Satisfiability: An Update 16:30‑17:00 Stefan Porschen, Tatjana Schmidt and Ewald Speckenmeyer Complexity Results for Linear XSAT Problems 17:00‑17:30 Olaf Beyersdorff, Arne Meier, Sebastian Mueller, Michael Thomas and Heribert Vollmer Proof Complexity of Propositional Default Logic
19:00‑22:00 Drinks reception at Edinburgh Castle