FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Abstract Interpretation	Sound up-to techniques and Complete abstract domains (PDF, talk)
Abstract syntax	Syntax and Semantics for Operations with Scopes (PDF, talk)
accumulated weight constraints	Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (PDF, talk)
additive monad	Dialectica models of type theory (PDF, talk)
algebra in type theory	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk)
algebraic effects	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (PDF, talk) Syntax and Semantics for Operations with Scopes (PDF, talk)
Algebraic Geometry	Polynomial Invariants for Affine Programs (PDF, talk)
algebraic structures	Free Higher Groups in Homotopy Type Theory (PDF, talk)
algorithmic complexity	A modal mu perspective on solving parity games in quasipolynomial time. (PDF, talk)
allegories	Allegories: decidability and graph homomorphisms (PDF, talk)
Alternating Automata	The State Complexity of Alternating Automata (PDF, talk)
applicative bisimulation distance	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (PDF, talk)
applicative simulation distance	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (PDF, talk)
applied lambda-calculus	Type-two polynomial-time and restricted lookahead. (PDF, talk)
arithmetic circuits	Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (PDF, talk)
Asynchronous Games	An Asynchronous Soundness Theorem for Concurrent Separation Logic (PDF, talk)
Automata over infinite words	One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata (PDF, talk)
Automata Theory	The State Complexity of Alternating Automata (PDF, talk)
automated complexity analysis	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
axiomatization	Riesz Modal Logic with Threshold Operators (PDF, talk) Allegories: decidability and graph homomorphisms (PDF, talk)
B
Behavioural metrics	A van Benthem Theorem for Fuzzy Modal Logic (PDF, talk)
Benchmarking	A Simple and Optimal Complementation Algorithm for Büchi Automata (PDF, talk)
Beth models	Computability Beyond Church-Turing via Choice Sequences (PDF, talk)
bisimulation	Quasi-Open Bisimilarity with Mismatch is Intuitionistic (PDF, talk)
boolean algebra	Classical realizability as a classifier for nondeterminism (PDF, talk)
Boolean-valued models	Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk)
Bounded expansion	Parameterized circuit complexity of model-checking on sparse structures (PDF, talk)
Böhm trees	Probabilistic Böhm Trees and Probabilistic Separation (PDF, talk)
Büchi Automaton	A Simple and Optimal Complementation Algorithm for Büchi Automata (PDF, talk)
C
call by value	Eager Functions as Processes (PDF, talk)
Categorical Logic	The Syntax and Semantics of Quantitative Type Theory (PDF, talk) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (PDF, talk)
Categorical model	Syntax and Semantics for Operations with Scopes (PDF, talk)
Categorical models	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (PDF, talk)
Categorical Quantum Mechanics	Two complete axiomatisations of pure-state qubit quantum computing (PDF, talk) A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (PDF, talk) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (PDF, talk)
Categorical semantics	A Logical Account for Linear Partial Differential Equations (PDF, talk) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (PDF, talk) A General Framework for Relational Parametricity (PDF, talk)
category theory	What's in a game? A theory of game models (PDF, talk) A Generalized Modality for Recursion (PDF, talk) Dialectica models of type theory (PDF, talk)
Causal Dependency	Causal Computational Complexity of Distributed Processes (PDF, talk)
cellular cohomology	Cellular Cohomology in Homotopy Type Theory (PDF, talk)
Choice sequences	Computability Beyond Church-Turing via Choice Sequences (PDF, talk)
choiceless polynomial time	On computability and tractability for infinite sets (PDF, talk)
Circuit complexity	Parameterized circuit complexity of model-checking on sparse structures (PDF, talk)
circuit satisfiability	Satisfiability in multi-valued circuits (PDF, talk)
classical arithmetic	A sequent calculus with dependent types for classical arithmetic (PDF, talk)
classical realizability	Classical realizability as a classifier for nondeterminism (PDF, talk) A sequent calculus with dependent types for classical arithmetic (PDF, talk)
clocks	Guarded Computational Type Theory (PDF, talk)
Coarse computability	An answer to the Gamma question (PDF, talk)
coherence theorems	Ribbon tensorial logic (PDF, talk)
coinduction	Every λ-Term is Meaningful for the Infinitary Relational Model (PDF, talk)
coinduction up-to	Sound up-to techniques and Complete abstract domains (PDF, talk)
combinators	Regular Transducer Expressions for Regular Transformations over infinite words (PDF, talk)
Complementation	A Simple and Optimal Complementation Algorithm for Büchi Automata (PDF, talk)
complete abstract domains	Sound up-to techniques and Complete abstract domains (PDF, talk)
complexity dichotomy	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
compositionality	Compositional game theory (PDF, talk)
Computability	An answer to the Gamma question (PDF, talk)
Computation Complexity	Causal Computational Complexity of Distributed Processes (PDF, talk)
Computation Tree Logic	Automaton-Based Criteria for Membership in CTL (PDF, talk)
computational complexity	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (PDF, talk)
computational monads	An algebraic theory of Markov processes (PDF, talk)
Computational thinking	Sequential Relational Decomposition (PDF, talk)
concurrency	ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (PDF, talk)
concurrency and distributed computation	Work Analysis with Resource-Aware Session Types (PDF, talk)
Concurrent games	The concurrent game semantics of Probabilistic PCF (PDF, talk)
Concurrent Process Calculi	Causal Computational Complexity of Distributed Processes (PDF, talk)
Concurrent Separation Logic	An Asynchronous Soundness Theorem for Concurrent Separation Logic (PDF, talk)
Concurrent strategies	What's in a game? A theory of game models (PDF, talk)
conditional value at risk	Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (PDF, talk)
Confusion	Concurrency and Probability: Removing Confusion, Compositionally (PDF, talk)
Conservativity	Around Classical and Intuitionistic Linear Logics (PDF, talk)
Constraint Satisfaction Problem	Satisfiability in multi-valued circuits (PDF, talk)
constraint satisfaction problems	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
constructive mathematics	Computable decision-making on the reals and other spaces via partiality and nondeterminism (PDF, talk)
contextuality	Logical paradoxes in quantum computation (PDF, talk)
Correspondence theory	A van Benthem Theorem for Fuzzy Modal Logic (PDF, talk)
counting classes	Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (PDF, talk)
cross-fertilization	Sound up-to techniques and Complete abstract domains (PDF, talk)
cubical type theory	On Higher Inductive Types in Cubical Type Theory (PDF, talk) Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk)
Curry-Howard	Classical realizability as a classifier for nondeterminism (PDF, talk)
cut elimination	Unification nets: canonical proof net quantifiers (PDF, talk)
cyber-physical systems	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (PDF, talk)
D
Data Races	An Asynchronous Soundness Theorem for Concurrent Separation Logic (PDF, talk)
data words	Logics for Word Transductions with Synthesis (PDF, talk) Playing with Repetitions in Data Words Using Energy Games (PDF, talk)
database theory	Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. (PDF, talk)
Decidability	Allegories: decidability and graph homomorphisms (PDF, talk)
definability	Definable decompositions for graphs of bounded linear cliquewidth (PDF, talk)
definable while programs	On computability and tractability for infinite sets (PDF, talk)
denotation	Every λ-Term is Meaningful for the Infinitary Relational Model (PDF, talk)
denotational semantics	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (PDF, talk) Probabilistic stable functions on discrete cones are power series. (PDF, talk) Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk)
dependent choice	A sequent calculus with dependent types for classical arithmetic (PDF, talk)
dependent product types	Dialectica models of type theory (PDF, talk)
Dependent Refinement Types	Dependent Temporal Effects and Fixpoint Logic for Verification (PDF, talk)
dependent temporal effects	Dependent Temporal Effects and Fixpoint Logic for Verification (PDF, talk)
dependent type theory	Dialectica models of type theory (PDF, talk)
dependent types	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (PDF, talk) A sequent calculus with dependent types for classical arithmetic (PDF, talk) Guarded Computational Type Theory (PDF, talk)
Description Logic	A van Benthem Theorem for Fuzzy Modal Logic (PDF, talk)
descriptive complexity	Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (PDF, talk) A modal mu perspective on solving parity games in quasipolynomial time. (PDF, talk)
determinacy	Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. (PDF, talk)
Deterministic Automata	One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata (PDF, talk)
Diagrammatic Reasoning	A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (PDF, talk) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (PDF, talk)
Dialectica interpretation	Dialectica models of type theory (PDF, talk)
differential dynamic logic	Differential Equation Axiomatization: The Impressive Power of Differential Ghosts (PDF, talk)
differential equation axiomatization	Differential Equation Axiomatization: The Impressive Power of Differential Ghosts (PDF, talk)
Differential Equations	A Logical Account for Linear Partial Differential Equations (PDF, talk)
differential ghosts	Differential Equation Axiomatization: The Impressive Power of Differential Ghosts (PDF, talk)
Differential Linear Logic	A Logical Account for Linear Partial Differential Equations (PDF, talk)
Digital libraries	Computability Beyond Church-Turing via Choice Sequences (PDF, talk)
Diller-Nahm variant	Dialectica models of type theory (PDF, talk)
display map category	Dialectica models of type theory (PDF, talk)
Distribution based objectives	Distribution-based objectives for Markov Decision Processes (PDF, talk)
Double negation	Around Classical and Intuitionistic Linear Logics (PDF, talk)
Double-pushout rewriting	Rewriting with Frobenius (PDF, talk)
downward closures	PTL-separability and closures for WQOs on words (PDF, talk)
duality	Riesz Modal Logic with Threshold Operators (PDF, talk)
dynamic logic	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (PDF, talk)
Dynamic nets	Concurrency and Probability: Removing Confusion, Compositionally (PDF, talk)
E
effectful bisimilarity	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (PDF, talk)
ellipsoid method	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem (PDF, talk)
energy games	Playing with Repetitions in Data Words Using Energy Games (PDF, talk)
enriched category theory	Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (PDF, talk)
equational logic	An algebraic theory of Markov processes (PDF, talk)
equivalence relations	Unary negation fragment with equivalence relations has the finite model property (PDF, talk)
erasure	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk)
Event structures	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (PDF, talk) The concurrent game semantics of Probabilistic PCF (PDF, talk)
expected shortfall	Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (PDF, talk)
expressiveness	A Theory of Register Monitors (PDF, talk)
extensive category	Dialectica models of type theory (PDF, talk)
F
feasibility of functionals	Type-two polynomial-time and restricted lookahead. (PDF, talk)
finite model property	Unary negation fragment with equivalence relations has the finite model property (PDF, talk)
finite model theory	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk) Model-Theoretic Characterizations of Boolean and Arithmetic Circuit Classes of Small Depth (PDF, talk)
finite sum types	Dialectica models of type theory (PDF, talk)
First order transduction	Regular and First Order List Functions (PDF, talk)
First-order list function	Regular and First Order List Functions (PDF, talk)
first-order logic	PTL-separability and closures for WQOs on words (PDF, talk)
First-order multiplicative linear logic	Unification nets: canonical proof net quantifiers (PDF, talk)
First-order types	On the number of types in sparse graphs (PDF, talk)
fixed-point logic	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem (PDF, talk)
fixpoint logic	Dependent Temporal Effects and Fixpoint Logic for Verification (PDF, talk)
Flow Analysis	Causal Computational Complexity of Distributed Processes (PDF, talk)
flows and nowhere-zero flows	A theory of linear typings as flows on 3-valent graphs (PDF, talk)
focusing	Strong Sums in Focused Logic (PDF, talk) Around Classical and Intuitionistic Linear Logics (PDF, talk)
Forest Algebra	MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras (PDF, talk)
Forest Algebras	Wreath Products of Distributive Forest Algebras (PDF, talk)
formal aspects of program analysis	Work Analysis with Resource-Aware Session Types (PDF, talk)
formal topology	Computable decision-making on the reals and other spaces via partiality and nondeterminism (PDF, talk)
formal verification	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (PDF, talk)
Frobenius algebra	Rewriting with Frobenius (PDF, talk)
full abstraction	Eager Functions as Processes (PDF, talk)
Functional Analysis	A Logical Account for Linear Partial Differential Equations (PDF, talk)
functional interpretation	Dialectica models of type theory (PDF, talk) A functional interpretation with state (PDF, talk)
functional programming	A Generalized Modality for Recursion (PDF, talk)
fuzz	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (PDF, talk)
Fuzzy logic	A van Benthem Theorem for Fuzzy Modal Logic (PDF, talk)
G
Game semantics	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (PDF, talk) The concurrent game semantics of Probabilistic PCF (PDF, talk) What's in a game? A theory of game models (PDF, talk) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (PDF, talk)
Game Theory	Compositional game theory (PDF, talk)
games and logic	Distribution-based objectives for Markov Decision Processes (PDF, talk)
generalised species	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (PDF, talk)
geometry of interaction	The Geometry of Computation-Graph Abstraction (PDF, talk)
gluing	Dialectica models of type theory (PDF, talk)
graph isomorphism	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem (PDF, talk)
graph theory	Allegories: decidability and graph homomorphisms (PDF, talk) A theory of linear typings as flows on 3-valent graphs (PDF, talk)
Graphical reasoning	Rewriting with Frobenius (PDF, talk)
Guarded Recursion	A Generalized Modality for Recursion (PDF, talk) Guarded Computational Type Theory (PDF, talk)
H
halting problem	A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (PDF, talk)
Handlers	Syntax and Semantics for Operations with Scopes (PDF, talk)
hereditarily definable sets	On computability and tractability for infinite sets (PDF, talk)
Hierarchy Theorem	The State Complexity of Alternating Automata (PDF, talk)
higher groups	Higher Groups in Homotopy Type Theory (PDF, talk)
higher inductive types	Impredicative Encodings of (Higher) Inductive Types (PDF, talk) On Higher Inductive Types in Cubical Type Theory (PDF, talk)
higher-order computability	Type-two polynomial-time and restricted lookahead. (PDF, talk)
higher-order programs	Dependent Temporal Effects and Fixpoint Logic for Verification (PDF, talk)
homotopy type theory	Impredicative Encodings of (Higher) Inductive Types (PDF, talk) Higher Groups in Homotopy Type Theory (PDF, talk) On Higher Inductive Types in Cubical Type Theory (PDF, talk) Cellular Cohomology in Homotopy Type Theory (PDF, talk) Free Higher Groups in Homotopy Type Theory (PDF, talk)
howe's method	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (PDF, talk)
hybrid logic	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (PDF, talk)
hybrid systems	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (PDF, talk)
I
impredicative encodings	Impredicative Encodings of (Higher) Inductive Types (PDF, talk)
impredicativity	Impredicative Encodings of (Higher) Inductive Types (PDF, talk)
inductive types	Impredicative Encodings of (Higher) Inductive Types (PDF, talk)
infinite-state systems	PTL-separability and closures for WQOs on words (PDF, talk)
information flow	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (PDF, talk)
integer weights	Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (PDF, talk)
intersection types	Every λ-Term is Meaningful for the Infinitary Relational Model (PDF, talk)
intersections	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk)
Intuitionistic linear logic	Around Classical and Intuitionistic Linear Logics (PDF, talk)
Intuitionistic logic	Quasi-Open Bisimilarity with Mismatch is Intuitionistic (PDF, talk)
irrelevance	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk)
K
Kakutani's fixed point theorem	Distribution-based objectives for Markov Decision Processes (PDF, talk)
L
lambda calculi	Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (PDF, talk)
lambda calculus	Probabilistic stable functions on discrete cones are power series. (PDF, talk) Eager Functions as Processes (PDF, talk)
lambda calculus and combinatory logic	A theory of linear typings as flows on 3-valent graphs (PDF, talk)
lambda-calculus	Every λ-Term is Meaningful for the Infinitary Relational Model (PDF, talk)
laziness	A sequent calculus with dependent types for classical arithmetic (PDF, talk)
Lean proof assistant	Higher Groups in Homotopy Type Theory (PDF, talk)
linear cliquewidth	Definable decompositions for graphs of bounded linear cliquewidth (PDF, talk)
linear logic	The Syntax and Semantics of Quantitative Type Theory (PDF, talk) Work Analysis with Resource-Aware Session Types (PDF, talk) Unification nets: canonical proof net quantifiers (PDF, talk) Around Classical and Intuitionistic Linear Logics (PDF, talk) LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (PDF, talk) A theory of linear typings as flows on 3-valent graphs (PDF, talk)
Linear Temporal Logic	Automaton-Based Criteria for Membership in CTL (PDF, talk) One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata (PDF, talk)
linear time hierarchy	A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (PDF, talk)
locale theory	Computable decision-making on the reals and other spaces via partiality and nondeterminism (PDF, talk)
logic	Logics for Word Transductions with Synthesis (PDF, talk)
logic for PTime	On computability and tractability for infinite sets (PDF, talk)
Logic on Trees	Wreath Products of Distributive Forest Algebras (PDF, talk)
Logical Frameworks	Strong Sums in Focused Logic (PDF, talk)
logical paradoxes	Logical paradoxes in quantum computation (PDF, talk)
logical predicates	Dialectica models of type theory (PDF, talk)
LOIS	On computability and tractability for infinite sets (PDF, talk)
Lower Bounds	The State Complexity of Alternating Automata (PDF, talk)
M
magic states	Logical paradoxes in quantum computation (PDF, talk)
Markov decision processes	Distribution-based objectives for Markov Decision Processes (PDF, talk) Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (PDF, talk) Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (PDF, talk)
Markov processes	An algebraic theory of Markov processes (PDF, talk)
Martin-L\"{o}f type theory	Impredicative Encodings of (Higher) Inductive Types (PDF, talk)
Martin-Löf type theory	Dialectica models of type theory (PDF, talk)
Matrix semigroups	Polynomial Invariants for Affine Programs (PDF, talk)
Mean-payoff games	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (PDF, talk)
mechanised theorem proving	Quasi-Open Bisimilarity with Mismatch is Intuitionistic (PDF, talk)
mechanized reasoning	Cellular Cohomology in Homotopy Type Theory (PDF, talk)
MMSNP	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
modal logic	Quasi-Open Bisimilarity with Mismatch is Intuitionistic (PDF, talk) A van Benthem Theorem for Fuzzy Modal Logic (PDF, talk)
modal mu	A modal mu perspective on solving parity games in quasipolynomial time. (PDF, talk)
modalities	Guarded Computational Type Theory (PDF, talk)
model checking	Distribution-based objectives for Markov Decision Processes (PDF, talk)
Model Theory	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
Model-checking first-order logic	Parameterized circuit complexity of model-checking on sparse structures (PDF, talk)
model-checking problems	Tree depth, quantifier elimination, and quantifier rank (PDF, talk)
modules	Strong Sums in Focused Logic (PDF, talk)
Monad	Syntax and Semantics for Operations with Scopes (PDF, talk)
monitoring	A Theory of Register Monitors (PDF, talk)
monoidal categories	Compositional game theory (PDF, talk) Two complete axiomatisations of pure-state qubit quantum computing (PDF, talk)
MSO	MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras (PDF, talk)
MSO on omega-Words	LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic (PDF, talk)
MSO transduction	Regular and First Order List Functions (PDF, talk)
multi-objective optimization	Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (PDF, talk)
N
N player games	Rational Synthesis Under Imperfect Information (PDF, talk)
Nash equilibrium	Rational Synthesis Under Imperfect Information (PDF, talk)
Negative translations	Around Classical and Intuitionistic Linear Logics (PDF, talk)
Non-Deterministic Automata	One Theorem to Rule Them All: A Unified Translation of LTL into $\omega$-Automata (PDF, talk)
non-idempotency	Every λ-Term is Meaningful for the Infinitary Relational Model (PDF, talk)
Non-lawlike computability	Computability Beyond Church-Turing via Choice Sequences (PDF, talk)
non-zero sum games	Rational Synthesis Under Imperfect Information (PDF, talk)
nondeterminism	Classical realizability as a classifier for nondeterminism (PDF, talk)
Nowhere dense graphs	On the number of types in sparse graphs (PDF, talk)
Nuprl proof assistant	Computability Beyond Church-Turing via Choice Sequences (PDF, talk)
O
observational equivalence	Probabilistic Böhm Trees and Probabilistic Separation (PDF, talk)
omega-languages	A Theory of Register Monitors (PDF, talk)
Omega-regular languages	Automaton-Based Criteria for Membership in CTL (PDF, talk)
open games	Compositional game theory (PDF, talk)
Optimal Upper Bound	A Simple and Optimal Complementation Algorithm for Büchi Automata (PDF, talk)
OR causality	Concurrency and Probability: Removing Confusion, Compositionally (PDF, talk)
oracle Turing machines	Type-two polynomial-time and restricted lookahead. (PDF, talk)
Origin	Logics for Word Transductions with Synthesis (PDF, talk)
P
parameterized AC^0	Tree depth, quantifier elimination, and quantifier rank (PDF, talk) A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (PDF, talk)
Parametricity	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk) A General Framework for Relational Parametricity (PDF, talk)
parity games	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (PDF, talk) A modal mu perspective on solving parity games in quasipolynomial time. (PDF, talk)
PDL	Wreath Products of Distributive Forest Algebras (PDF, talk)
Persistent places	Concurrency and Probability: Removing Confusion, Compositionally (PDF, talk)
Petri nets	Concurrency and Probability: Removing Confusion, Compositionally (PDF, talk)
pi calculus	Eager Functions as Processes (PDF, talk)
pi-calculus	Quasi-Open Bisimilarity with Mismatch is Intuitionistic (PDF, talk)
pointfree topology	Computable decision-making on the reals and other spaces via partiality and nondeterminism (PDF, talk)
polymorphism	Impredicative Encodings of (Higher) Inductive Types (PDF, talk)
polynomial functor	Dialectica models of type theory (PDF, talk)
Polynomial functors	What's in a game? A theory of game models (PDF, talk)
polynomial-time tractability	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
presheaf semantics	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk)
Presheaves	What's in a game? A theory of game models (PDF, talk)
Prime Numbers	The State Complexity of Alternating Automata (PDF, talk)
Probabilistic computation	Probabilistic stable functions on discrete cones are power series. (PDF, talk)
probabilistic CTL	Riesz Modal Logic with Threshold Operators (PDF, talk)
probabilistic finite automata	Distribution-based objectives for Markov Decision Processes (PDF, talk)
probabilistic lambda-calculus	Probabilistic Böhm Trees and Probabilistic Separation (PDF, talk)
Probabilistic programs	The concurrent game semantics of Probabilistic PCF (PDF, talk)
probabilistic systems	Distribution-based objectives for Markov Decision Processes (PDF, talk)
probabilistic verification	Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes (PDF, talk)
profunctor	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (PDF, talk)
Program Analysis	Polynomial Invariants for Affine Programs (PDF, talk)
Program extraction	A functional interpretation with state (PDF, talk)
Program invariant	Polynomial Invariants for Affine Programs (PDF, talk)
program refinement	ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (PDF, talk)
programming language semantics	Work Analysis with Resource-Aware Session Types (PDF, talk) Computable decision-making on the reals and other spaces via partiality and nondeterminism (PDF, talk)
programming languages	Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (PDF, talk)
progress measure	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (PDF, talk)
Proof nets	Unification nets: canonical proof net quantifiers (PDF, talk)
proof-as-program	Classical realizability as a classifier for nondeterminism (PDF, talk)
proofs-as-programs	A sequent calculus with dependent types for classical arithmetic (PDF, talk)
Propositional Dynamic Logic	Wreath Products of Distributive Forest Algebras (PDF, talk)
PROPs	Rewriting with Frobenius (PDF, talk)
Q
quantale relator	Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (PDF, talk)
quantifier rank	Tree depth, quantifier elimination, and quantifier rank (PDF, talk)
quantifiers	Unification nets: canonical proof net quantifiers (PDF, talk)
quantitative algebraic reasoning	An algebraic theory of Markov processes (PDF, talk)
quantum computation	Logical paradoxes in quantum computation (PDF, talk) Two complete axiomatisations of pure-state qubit quantum computing (PDF, talk)
Quantum Computing	A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics (PDF, talk) Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics (PDF, talk) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (PDF, talk)
quantum program	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (PDF, talk)
query	Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. (PDF, talk)
Query Enumeration	MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras (PDF, talk)
R
Ramsey theory	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
random variables	Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk)
ranking functions	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
Rational synthesis	Rational Synthesis Under Imperfect Information (PDF, talk)
real-time	A Theory of Register Monitors (PDF, talk)
Realizability	Classical realizability as a classifier for nondeterminism (PDF, talk)
recognizability	Definable decompositions for graphs of bounded linear cliquewidth (PDF, talk)
register machines	A Theory of Register Monitors (PDF, talk)
regular expressions	Regular Transducer Expressions for Regular Transformations over infinite words (PDF, talk)
regular languages	PTL-separability and closures for WQOs on words (PDF, talk)
relational model	Every λ-Term is Meaningful for the Infinitary Relational Model (PDF, talk)
relational reasoning	ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (PDF, talk)
resource calculus	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (PDF, talk)
ribbon categories	Ribbon tensorial logic (PDF, talk)
Riesz modal logic	Riesz Modal Logic with Threshold Operators (PDF, talk)
S
Satisfiability	Unary negation fragment with equivalence relations has the finite model property (PDF, talk)
semantics	Every λ-Term is Meaningful for the Infinitary Relational Model (PDF, talk)
semantics of programming languages	The Geometry of Computation-Graph Abstraction (PDF, talk)
semidefinite programming	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem (PDF, talk)
separability	PTL-separability and closures for WQOs on words (PDF, talk)
separation	Probabilistic Böhm Trees and Probabilistic Separation (PDF, talk)
separation logic	ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency (PDF, talk)
sequent calculus	A sequent calculus with dependent types for classical arithmetic (PDF, talk)
Sequential algorithms	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (PDF, talk)
sequential types	Every λ-Term is Meaningful for the Infinitary Relational Model (PDF, talk)
sets with atoms	On computability and tractability for infinite sets (PDF, talk)
smart grid	A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow (PDF, talk)
solving equations	Satisfiability in multi-valued circuits (PDF, talk)
sound up-to techniques	Sound up-to techniques and Complete abstract domains (PDF, talk)
Stability	On the number of types in sparse graphs (PDF, talk)
State Complexity	The State Complexity of Alternating Automata (PDF, talk)
state injection	Logical paradoxes in quantum computation (PDF, talk)
State monad	A functional interpretation with state (PDF, talk)
stochastic lambda calculus	Boolean-Valued Semantics for Stochastic Lambda-Calculus (PDF, talk)
stochastic shortest path	Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes (PDF, talk)
Stone space	On the number of types in sparse graphs (PDF, talk)
Streaming string transducers	Regular and First Order List Functions (PDF, talk)
Streams	A Generalized Modality for Recursion (PDF, talk)
string diagrams	Rewriting with Frobenius (PDF, talk) Two complete axiomatisations of pure-state qubit quantum computing (PDF, talk) Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams (PDF, talk)
strong sums	Strong Sums in Focused Logic (PDF, talk)
structure theory	Satisfiability in multi-valued circuits (PDF, talk)
succinct ordered tree coding	A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games (PDF, talk)
sums-of-squares	Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem (PDF, talk)
Symmetric monoidal categories	Rewriting with Frobenius (PDF, talk)
Synchronous Programming	A Generalized Modality for Recursion (PDF, talk)
Synthesis	Logics for Word Transductions with Synthesis (PDF, talk)
System Composition	Sequential Relational Decomposition (PDF, talk)
system F	Impredicative Encodings of (Higher) Inductive Types (PDF, talk)
Systems decomposition	Sequential Relational Decomposition (PDF, talk)
T
Taylor expansion	Species, Profunctors and Taylor Expansion Weighted by SMCC--A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs-- (PDF, talk)
temporal logic of repeating values	Playing with Repetitions in Data Words Using Energy Games (PDF, talk)
Temporal Verification	Dependent Temporal Effects and Fixpoint Logic for Verification (PDF, talk)
Tensor logic	Around Classical and Intuitionistic Linear Logics (PDF, talk)
tensorflow	The Geometry of Computation-Graph Abstraction (PDF, talk)
tensorial logic	Ribbon tensorial logic (PDF, talk)
termination	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
the MRDP theorem	A parameterized halting problem, the linear time hierarchy, and the MRDP theorem (PDF, talk)
Theory of Computation	A General Framework for Relational Parametricity (PDF, talk)
transducers	Regular Transducer Expressions for Regular Transformations over infinite words (PDF, talk)
transduction	Definable decompositions for graphs of bounded linear cliquewidth (PDF, talk) Logics for Word Transductions with Synthesis (PDF, talk)
tree automata	Automaton-Based Criteria for Membership in CTL (PDF, talk)
tree-depth	Tree depth, quantifier elimination, and quantifier rank (PDF, talk)
Trees	MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras (PDF, talk)
true concurrency	An Asynchronous Soundness Theorem for Concurrent Separation Logic (PDF, talk)
truncation levels	Free Higher Groups in Homotopy Type Theory (PDF, talk)
Turing degrees	An answer to the Gamma question (PDF, talk)
Two player games	Playing with Repetitions in Data Words Using Energy Games (PDF, talk)
two-variable logic	Weighted model counting beyond two-variable logic (PDF, talk)
type system	Causal Computational Complexity of Distributed Processes (PDF, talk)
type systems	Work Analysis with Resource-Aware Session Types (PDF, talk) A Generalized Modality for Recursion (PDF, talk) A theory of linear typings as flows on 3-valent graphs (PDF, talk)
type theory	The Syntax and Semantics of Quantitative Type Theory (PDF, talk) Computability Beyond Church-Turing via Choice Sequences (PDF, talk) Guarded Computational Type Theory (PDF, talk)
U
unambiguous	Regular Transducer Expressions for Regular Transformations over infinite words (PDF, talk)
unary negation fragment	Unary negation fragment with equivalence relations has the finite model property (PDF, talk)
unification	Unification nets: canonical proof net quantifiers (PDF, talk)
uniform one-dimensional fragment	Weighted model counting beyond two-variable logic (PDF, talk)
Uniform quasi-wideness	On the number of types in sparse graphs (PDF, talk)
unions	Degrees of Relatedness - A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory (PDF, talk)
univalent foundations	On Higher Inductive Types in Cubical Type Theory (PDF, talk)
universal algebra	A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP (PDF, talk)
universes	Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (PDF, talk) Guarded Computational Type Theory (PDF, talk)
V
VC-density	On the number of types in sparse graphs (PDF, talk)
VC-dimension	On the number of types in sparse graphs (PDF, talk)
vector addition systems with states	Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS (PDF, talk)
view	Can One Escape Red Chains? Regular Path Queries Determinacy is Undecidable. (PDF, talk)
W
weighted model counting	Weighted model counting beyond two-variable logic (PDF, talk)
while programs with atoms	On computability and tractability for infinite sets (PDF, talk)
Wreath Products	Wreath Products of Distributive Forest Algebras (PDF, talk)
Z
Zariski topology	Polynomial Invariants for Affine Programs (PDF, talk)

Disclaimer | Powered by EasyChair Smart Program