LICS PROGRAM
Days: Monday, July 9th Tuesday, July 10th Wednesday, July 11th Thursday, July 12th
Monday, July 9th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:30 Session 46: FLoC Plenary Lecture: Peter O'Hearn
Chair:
Location: Maths LT1
| 09:00 | Continuous Reasoning: Scaling the Impact of Formal Methods (abstract) |
10:30-11:00Coffee Break
11:00-12:40 Session 47D
Chair:
Location: Maths LT1
| 11:00 | Definable decompositions for graphs of bounded linear cliquewidth (abstract)   |
| 11:20 | Parameterized circuit complexity of model-checking on sparse structures (abstract) |
| 11:40 | Sequential Relational Decomposition (abstract) |
| 12:00 | A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (abstract) |
| 12:20 | Regular and First Order List Functions (abstract) |
11:00-12:40 Session 47E
Chair:
Location: Maths LT3
| 11:00 | A theory of linear typings as flows on 3-valent graphs (abstract) |
| 11:20 | Cellular Cohomology in Homotopy Type Theory (abstract) |
| 11:40 | Free Higher Groups in Homotopy Type Theory (abstract) |
| 12:00 | Higher Groups in Homotopy Type Theory (abstract) |
| 12:20 | Strong Sums in Focused Logic (abstract) |
12:30-14:00Lunch Break
14:00-15:40 Session 49D
Chair:
Location: Maths LT1
| 14:00 | A modal mu perspective on solving parity games in quasipolynomial time. (abstract) |
| 14:20 | A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (abstract) |
| 14:40 | Rational Synthesis Under Imperfect Information (abstract) |
| 15:00 | Playing with Repetitions in Data Words Using Energy Games (abstract) |
| 15:20 | Compositional game theory (abstract) |
14:00-15:40 Session 49E
Chair:
Location: Maths LT3
| 14:00 | Concurrency and Probability: Removing Confusion, Compositionally (abstract) |
| 14:20 | ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (abstract) |
| 14:40 | Eager Functions as Processes (abstract) |
| 15:00 | Quasi-Open Bisimilarity with Mismatch is Intuitionistic (abstract) |
| 15:20 | Causal Computational Complexity of Distributed Processes (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 51D
Chair:
Location: Maths LT1
| 16:00 | One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata (abstract) |
| 16:20 | A Simple and Optimal Complementation Algorithm for Büchi Automata (abstract) |
| 16:40 | The State Complexity of Alternating Automata (abstract) |
| 17:00 | Automaton-Based Criteria for Membership in CTL (abstract) |
| 17:20 | Separability by piecewise testable languages and downward closures beyond subwords (abstract) |
| 17:40 | Regular Transducer Expressions for Regular Transformations over infinite words (abstract) |
16:00-18:00 Session 51E
Chair:
Location: Maths LT3
| 16:00 | Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (abstract) |
| 16:20 | An algebraic theory of Markov processes (abstract) |
| 16:40 | Boolean-Valued Semantics for Stochastic Lambda-Calculus (abstract) |
| 17:00 | Sound up-to techniques and Complete abstract domains (abstract) |
| 17:20 | Every λ-Term is Meaningful for the Infinitary Relational Model (abstract) |
| 17:40 | Probabilistic Böhm Trees and Probabilistic Separation (abstract) |
19:00-21:30 FLoC reception at Ashmolean Museum
FLoC reception at Ashmolean Museum. Drinks and canapés available from 7pm (pre-booking via FLoC registration system required; guests welcome).
Location: Ashmolean Museum
Tuesday, July 10th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:00 Session 52D: LICS Invited Talk: Ursula Martin
Chair:
Location: Maths LT1
| 09:00 | On Diversity (abstract) |
10:00-10:40 Session 53B
Chair:
Location: Maths LT1
| 10:00 | Polynomial Invariants for Affine Programs (abstract) |
| 10:20 | An answer to the Gamma question (abstract) |
10:30-11:00Coffee Break
11:00-12:40 Session 54D
Chair:
Location: Maths LT1
| 11:00 | On the number of types in sparse graphs (abstract) |
| 11:20 | Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (abstract) |
| 11:40 | Tree depth, quantifier elimination, and quantifier rank (abstract) |
| 12:00 | Wreath Products of Distributive Forest Algebras (abstract) |
| 12:20 | MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras (abstract) |
11:00-12:40 Session 54E
Chair:
Location: Maths LT3
| 11:00 | Impredicative Encodings of (Higher) Inductive Types (abstract) |
| 11:20 | Guarded Computational Type Theory (abstract) |
| 11:40 | Work Analysis with Resource-Aware Session Types (abstract) |
| 12:00 | A General Framework for Relational Parametricity (abstract) |
| 12:20 | Classical realizability as a classifier for nondeterminism (abstract) |
12:30-14:00Lunch Break
14:00-15:20 Session 55D
Chair:
Location: Maths LT1
| 14:00 | A van Benthem Theorem for Fuzzy Modal Logic (abstract) |
| 14:20 | Riesz Modal Logic with Threshold Operators (abstract) |
| 14:40 | Logics for Word Transductions with Synthesis (abstract) |
| 15:00 | Type-two polynomial-time and restricted lookahead. (abstract) |
14:00-15:20 Session 55E
Chair:
Location: Maths LT3
| 14:00 | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (abstract) |
| 14:20 | A Logical Account for Linear Partial Differential Equations (abstract) |
| 14:40 | Unification nets: canonical proof net quantifiers (abstract) |
| 15:00 | Around Classical and Intuitionistic Linear Logics (abstract) |
15:30-16:00Coffee Break
15:40-16:40 Session 57B
Chair:
Location: Maths LT1
| 15:40 | Distribution-based objectives for Markov Decision Processes (abstract) |
| 16:00 | Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (abstract) |
| 16:20 | Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (abstract) |
15:40-16:40 Session 57C
Chair:
Location: Maths LT3
| 15:40 | What's in a game? A theory of game models (abstract) |
| 16:00 | An Asynchronous Soundness Theorem for Concurrent Separation Logic (abstract) |
| 16:20 | The concurrent game semantics of Probabilistic PCF (abstract) |
17:00-18:30 Session 59: FLoC Public Lecture: Stuart Russell
Doors open at 4:30 pm; please be seated by 4:50 pm (attendance is free of charge and all are welcome; please register).
Chair:
Location: Sheldonian Theatre
| 17:00 | Unifying Logic and Probability: the BLOG Language (abstract) |
Wednesday, July 11th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:00 Session 60E: LICS Invited Talk: Thierry Coquand
Chair:
Location: Maths LT1
| 09:00 | Univalent Type Theory (abstract) |
10:00-10:40 Session 61
Chair:
Location: Maths LT1
| 10:00 | A sequent calculus with dependent types for classical arithmetic (abstract) |
| 10:20 | On Higher Inductive Types in Cubical Type Theory (abstract) |
10:30-11:00Coffee Break
11:00-12:40 Session 64D
Chair:
Location: Maths LT1
| 11:00 | Weighted model counting beyond two-variable logic (abstract) |
| 11:20 | A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (abstract) |
| 11:40 | Unary negation fragment with equivalence relations has the finite model property (abstract) |
| 12:00 | Satisfiability in multi-valued circuits (abstract) |
| 12:20 | Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. (abstract) |
11:00-12:40 Session 64E
Chair:
Location: Maths LT3
| 11:00 | Dialectica models of type theory (abstract) |
| 11:20 | Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (abstract) |
| 11:40 | A Fixpoint Logic and Dependent Effects for Temporal Property Verification (abstract) |
| 12:00 | Computability Beyond Church-Turing via Choice Sequences (abstract) |
| 12:20 | The Syntax and Semantics of Quantitative Type Theory (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 66A: FLoC Keynote Lecture: Shafi Goldwasser
Chair:
Location: Maths LT1
| 14:00 | Pseudo deterministic algorithms and proofs (abstract) |
15:30-16:00Coffee Break
17:00-18:30 Session 69B: LICS Award Session & Martin Hofmann Memorial
Chair:
Location: Maths LT1
| 17:00 | LICS Awards: The Kleene Award and the Test of Time Award (abstract) |
| 17:45 | Remembering Martin Hofmann (abstract) |
19:00-21:30 FLoC banquet at Examination Schools
FLoC banquet at Examination Schools. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).
Location: Examination Schools
Thursday, July 12th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:00-10:40 Session 70D
Chair:
Location: Maths LT1
| 09:00 | Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (abstract) |
| 09:20 | Logical paradoxes in quantum computation (abstract) |
| 09:40 | A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (abstract) |
| 10:00 | Two complete axiomatisations of pure-state qubit quantum computing (abstract) |
| 10:20 | Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (abstract) |
09:00-10:40 Session 70E
Chair:
Location: Maths LT3
| 09:00 | Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (abstract) |
| 09:20 | A Generalized Modality for Recursion (abstract) |
| 09:40 | A functional interpretation with state (abstract) |
| 10:00 | The Geometry of Computation-Graph Abstraction (abstract) |
| 10:20 | Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (abstract) |
10:30-11:00Coffee Break
11:00-12:00 Session 74D: LICS Invited Talk: Val Tannen
Chair:
Location: Maths LT1
| 11:00 | Provenance Analysis for First-order Model Checking (abstract) |
12:00-12:40 Session 75A
Chair:
Location: Maths LT1
| 12:00 | On computability and tractability for infinite sets (abstract) |
| 12:20 | Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem (abstract) |
12:30-14:00Lunch Break
14:00-15:40 Session 76E
Chair:
Location: Maths LT1
| 14:00 | Computable decision making on the reals and other spaces via partiality and nondeterminism (abstract) |
| 14:20 | A Theory of Register Monitors (abstract) |
| 14:40 | Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (abstract) |
| 15:00 | A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (abstract) |
| 15:20 | Differential Equation Axiomatization: The Impressive Power of Differential Ghosts (abstract) |
14:00-15:40 Session 76F
Chair:
Location: Maths LT3
| 14:00 | Probabilistic stable functions on discrete cones are power series. (abstract) |
| 14:20 | Allegories: decidability and graph homomorphisms (abstract) |
| 14:40 | Syntax and Semantics for Operations with Scopes (abstract) |
| 15:00 | Rewriting with Frobenius (abstract) |
| 15:20 | Ribbon tensorial logic (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 78C: LICS Invited Talk: Javier Esparza
Chair:
Location: Maths LT1
| 16:00 | Verification of population protocols (abstract) |
17:00-17:45 Session 81B: Alonzo Church Award Session
Chair:
Location: Maths LT1
| 17:00 | The 2018 Alonzo Church Award for Outstanding Contributions to Logic and Computation (abstract) |
| 17:15 | Constraints, Graphs, Algebra, Logic, and Complexity (abstract) |