FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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
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
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
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
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
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
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
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).

Tuesday, July 10th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

10:00-10:40 Session 53B
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
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
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
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
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
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).

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

10:00-10:40 Session 61
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
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
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).

Thursday, July 12th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:40 Session 70D
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
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
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
17:00-17:45 Session 81B: Alonzo Church Award Session
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)