FLoC on Monday, July 12th

See also the by session program.

ITP	LICS	RTA	SAT
09:00‑10:00 Gerwin Klein (NICTA) A Formally Verified OS Kernel. Now What?	09:00‑10:00 Martin Abadi (Microsoft Research and UCSC) The Fine print of Security	09:00‑10:00 Mikolaj Bojanczyk (Warsaw University) Invited Talk: Automata for Data Words and Data Trees	09:00‑10:00 Ramamohan Paturi. Exact Algorithms and Complexity
10:00‑10:30 Coffee break
10:30‑11:00 Joe Hendrix, Deepak Kapur and Jose Meseguer Coverset Induction with Partiality and Subsorts: a Powerlist Case Study 11:00‑11:30 Michaël Armand, Benjamin Grégoire, Arnaud Spiwack and Laurent Théry Extending Coq with Imperative Features and its Application to SAT Verification 11:30‑12:00 Moa Johansson, Lucas Dixon and Alan Bundy Case-Analysis for Rippling and Inductive Proof 12:00‑12:30 Panagiotis Manolios and Daron Vroon Interactive Termination Proofs using Termination Cores	10:30‑11:00 Joerg Endrullis, Dimitri Hendriks and Jan Willem Klop Modular Construction of Fixed Point Combinators and Clocked Boehm Trees 11:00‑11:30 Christopher Broadbent, Arnaud Carayol, C.-H. Luke Ong and Olivier Serre Recursion Schemes and Logical Reflection 11:30‑12:00 James Brotherston and Max Kanovich, Dominique Larchey-Wendling and Didier Galmiche. Undecidability of Boolean BI, and of propositional separation logic and its neighbours 12:00‑12:30 Paul-André Melliès Segal condition meets computational effects	10:30‑11:00 Alessio Guglielmi, Tom Gundersen and Michel Parigot A proof calculus which reduces syntactic bureaucracy 11:00‑11:30 Claus Appel, Vincent van Oostrom and Jakob Grue Simonsen Higher-Order (Non-)Modularity 11:30‑12:00 Ken-etsu Fujita and Aleksy Schubert The undecidability of type related problems in type-free style System F 12:00‑12:30 Manfred Schmidt-Schauss, David Sabel and Elena Machkasova Simulation in the Call-by-Need Lambda-Calculus with letrec	10:30‑11:00 Evgeny Dantsin and Alexander Wolpert On Moderately Exponential Time for SAT 11:00‑11:30 Eli Ben-Sasson and Jan Johannsen Lower bounds for width-restricted clause learning on small width formulas 11:30‑11:50 Scott Cotton Some Techniques for Minimizing Resolution Proofs 11:50‑12:10 Allen Van Gelder and Ivor Spence Zero-One Designs Produce Small Hard SAT Instances 12:10‑12:30 William Matthews and Ramamohan Paturi Uniquely Satisfiable k-SAT Instances with Almost Minimal Occurrences of Each Variable
12:30‑14:00 Lunch
14:00‑14:30 Gilles Barthe, Benjamin Grégoire and Santiago Zanella Béguelin Programming language techniques for cryptographic proofs 14:30‑15:00 David Cachera and David Pichardie Proof Pearl: A Certified Denotational Abstract Interpreter	14:00‑14:30 Dietrich Kuske, Jiamou Liu and Markus Lohrey The Isomorphism Problem On Classes of Automatic Structures 14:30‑15:00 Yuguo He On the strictness of the first-order quantifier structure hierarchy over finite structures	14:00‑15:00 Vincent van Oostrom (Utrecht University) Invited Talk: Realising Optimal Sharing	14:00‑14:30 Carsten Fuhs and Peter Schneider-Kamp Synthesizing Shortest Straight-Line Programs over GF(2) using SAT 14:30‑14:50 Oliver Kullmann Green-Tao Numbers and SAT
15:00‑15:30 Coffee break
15:30‑16:00 Sol Swords and Warren Hunt A Mechanically Verified AIG-to-BDD Conversion Algorithm 16:00‑16:30 William Mansky and Elsa Gunter A Framework for Formal Verification of Compiler Optimizations 16:30‑17:00 Herman Geuvers, Adam Koprowski, Dan Synek and Eelis van der Weegen Automated Machine-Checked Hybrid System Safety Proofs 17:00‑18:00 Business Meeting	15:30‑16:00 Martin Grohe Fixed-Point Definability and Polynomial Time on Graphs with Excluded Minors 16:00‑16:30 Stephan Kreutzer and Siamak Tazari Lower Bounds for the Complexity of Monadic Second-Order Logic 16:30‑17:00 Bastian Laubner Capturing Polynomial Time on Interval Graphs 17:15‑17:45 Patricia Johann, Alex Simpson and Janis Voigtländer A Generic Operational Metatheory for Algebraic Effects 17:45‑18:15 Noam Zeilberger Polarity and the logic of delimited continuations 18:30‑20:00 LICS Business Meeting and 25th Year Anniversary Celebration	16:00‑16:30 Samuel Mimram Computing Critical Pairs in 2-Dimensional Rewriting Systems 16:30‑17:00 Jordi Levy and Mateu Villaret An Efficient Nominal Unification Algorithm 17:15‑18:15 RTA Business Meeting	15:30‑16:00 Uwe Bubeck and Hans Kleine Büning Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN 16:00‑16:30 Christian Miller, Stefan Kupferschmid, Matthew Lewis and Bernd Becker Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs 16:30‑17:00 Enrico Giunchiglia, Paolo Marin and Massimo Narizzano sQueezeBF: An effective preprocessor for QBFs 17:00‑17:20 Alexandra Goultiaeva and Fahiem Bacchus Exploiting Circuit Representations in QBF solving