FLoC on Tuesday, July 13th

See also the by session program.

ITP	LICS	RTA	SAT
09:00‑10:00 Georg Gottlob (University of Oxford) Datalog+-: A Family of Logical Query Languages for New Applications.
10:00‑10:30 Coffee break
10:30‑11:00 Amy Felty and Brigitte Pientka Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison 11:00‑11:30 Serge Autexier and Dominik Dietrich A tactic language for declarative proofs 11:30‑12:00 Daria Walukiewicz-Chrząszcz and Jacek Chrząszcz Inductive Consequences in the Calculus of Constructions 12:00‑12:10 Magnus O. Myreen Separation logic adapted for proofs by rewriting 12:10‑12:20 Douglas Howe Higher-Order Abstract Syntax in Isabelle/HOL 12:20‑12:30 Bas Spitters and Eelis van der Weegen Developing the algebraic hierarchy with type classes in Coq	10:30‑11:00 Mikołaj Bojańczyk and Sławomir Lasota An extension of data automata that captures XPath 11:00‑11:30 Thomas Place and Luc Segoufin Deciding definability in FO2(<) on trees 11:30‑12:00 Luis Barguñó, Carles Creus, Guillem Godoy, Florent Jacquemard and Camille Vacher The Emptiness Problem for Tree Automata with Global Constraints 12:00‑12:30 Nicole Schweikardt and Luc Segoufin Addition-invariant FO and regularity	10:30‑11:00 Joerg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop and Vincent van Oostrom Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting 11:00‑11:30 Patrick Bahr Abstract Models of Transfinite Reductions 11:30‑12:00 Stefan Kahrs Infinitary Rewriting: Foundations Revisited 12:00‑12:30 Jakob Grue Simonsen Weak Convergence and Uniform Normalization in Infinitary Rewriting	10:30‑11:00 Vishwambhar Rathi, Erik Aurell, Lars Rasmussen and Mikael Skoglund Bounds on Threshold of Regular Random $k$-SAT 11:00‑11:30 Thomas Hugel and Yacine Boufkhad Non Uniform Selection of Solutions for Upper Bounding the 3-SAT Threshold 11:30‑11:50 Mladen Nikolic Statistical Methodology for Comparison of SAT Solvers 11:50‑12:10 Adrian Balint and Andreas Fröhlich Improving stochastic local search for SAT with instance specific information and a new probability distribution 12:10‑12:30 Anton Belov and Zbigniew Stachniak Improved Local Search for Circuit Satisfiability
12:30‑14:00 Lunch
14:00‑15:00 J Strother Moore (University of Texas) Theorem Proving for Verification: The Early Days.
15:00‑15:30 Coffee break
15:30‑18:00 Excursion [Information] [sign-up]	15:30‑16:00 Alessio Guglielmi, Tom Gundersen and Lutz Strassburger Breaking Paths in Atomic Flows for Classical Logic 16:00‑16:30 Michele Basaldella and Kazushige Terui Infinitary completeness in ludics 16:30‑17:00 Arnon Avron, Ofer Arieli and Anna Zamansky On Strong Maximality of Paraconsistent Finite-Valued Logics 17:15‑17:25 Mohamed Nabih Menaa On the Compositionality of Round Abstraction 17:25‑17:35 Pierre-yves Strub and Qian Wang Coq Modulo Theory - Short Paper 17:35‑17:45 Stanislav Böhm, Stefan Göller and Petr Jancar Bisimilarity of one-counter processes is PSPACE-complete 17:45‑17:55 Jian-Qi Li A Computability Path Ordering for Polymorphic Terms	15:30‑16:00 Harald Zankl and Martin Korp Modular Complexity Analysis via Relative Complexity 16:00‑16:30 Martin Avanzini and Georg Moser Closing the Gap Between Runtime Complexity and Polytime Computability 16:30‑17:00 Johannes Waldmann Polynomially Bounded Matrix Interpretations 17:00‑17:20 Sarah Winkler, Haruhiko Sato, Aart Middeldorp and Masahito Kurihara Optimizing mkbTT (System Description)	15:30‑16:00 Robert Brummayer, Florian Lonsing and Armin Biere Automated Testing and Debugging of SAT and QBF Solvers 16:00‑16:30 William Klieber, Samir Sapra, Sicun Gao and Edmund Clarke A Non-Prenex, Non-Clausal QBF Solver with Game-State Learning 16:30‑17:00 Florian Lonsing and Armin Biere Integrating Dependency Schemes in Search-Based QBF Solvers 17:00‑18:00 SAT Business meeting
19:00‑23:00 FLoC Banquet at Our Dynamic Earth