On this page:
Invited Speakers
- Thierry Coquand
Inner Models of Univalence - Javier Esparza
Black Ninjas in the Dark: Formal Analysis of Population Protocols - Peter W. O'Hearn
Continuous Reasoning: Scaling the impact of formal methods
Invited Papers
- Michael Blondin Javier Esparza Stefan Jaax Antonín Kucera
Black Ninjas in the Dark: Formal Analysis of Population ProtocolsMore Information... - Thierry Coquand
Inner Models of UnivalenceMore Information... - Peter W. O'Hearn
Continuous Reasoning: Scaling the impact of formal methodsMore Information...
Presented Papers
Entries are ordered by surname of first author
- S. Akshay Blaise Genest Nikhil Vyas
Distribution-based objectives for Markov Decision ProcessesMore Information... - Joël D. Allred Ulrich Ultes-Nitsche
A Simple and Optimal Complementation Algorithm for Büchi AutomataMore Information... - Robert Atkey
Syntax and Semantics of Quantitative Type TheoryMore Information... - Albert Atserias Joanna Ochremiak
Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism ProblemMore Information... - Steve Awodey Jonas Frey Sam Speight
Impredicative Encodings of (Higher) Inductive TypesMore Information... - Giorgio Bacci Robert Furber Dexter Kozen Radu Mardare Prakash Panangaden Dana Scott
Boolean-Valued Semantics for the Stochastic λ-CalculusMore Information... - Giorgio Bacci Radu Mardare Prakash Panangaden Gordon D. Plotkin
An Algebraic Theory of Markov ProcessesMore Information... - Christel Baier Nathalie Bertrand Clemens Dubslaff Daniel Gburek Ocan Sankur
Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision ProcessesMore Information... - Mark Bickford Liron Cohen Robert L. Constable Vincent Rahli
Computability Beyond Church-Turing via Choice SequencesMore Information... - Valentin Blot Jim Laird
Extensional and Intensional Semantic Universes: A Denotational Model of Dependent TypesMore Information... - Manuel Bodirsky Florent R. Madelaine Antoine Mottet
A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNPMore Information... - Brandon Bohrer André Platzer
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information FlowMore Information... - Mikolaj Bojanczyk Laure Daviaud Shankara Narayanan Krishna
Regular and First-Order List FunctionsMore Information... - Mikolaj Bojanczyk Martin Grohe Michal Pilipczuk
Definable decompositions for graphs of bounded linear cliquewidthMore Information... - Mikolaj Bojanczyk Szymon Torunczyk
On computability and tractability for infinite setsMore Information... - Udi Boker Yariv Shaulian
Automaton-Based Criteria for Membership in CTLMore Information... - Filippo Bonchi Fabio Gadducci Aleks Kissinger Pawel Sobocinski Fabio Zanasi
Rewriting with FrobeniusMore Information... - Filippo Bonchi Pierre Ganty Roberto Giacobazzi Dusko Pavlovic
Sound up-to techniques and Complete abstract domainsMore Information... - Tomás Brázdil Krishnendu Chatterjee Antonín Kucera Petr Novotný Dominik Velan Florian Zuleger
Efficient Algorithms for Asymptotic Bounds on Termination Time in VASSMore Information... - Roberto Bruni Hernán C. Melgratti Ugo Montanari
Concurrency and Probability: Removing Confusion, CompositionallyMore Information... - Ulrik Buchholtz Floris van Doorn Egbert Rijke
Higher Groups in Homotopy Type TheoryMore Information... - Ulrik Buchholtz Kuen-Bang Hou (Favonia)
Cellular Cohomology in Homotopy Type TheoryMore Information... - Simon Castellan Pierre Clairambault Hugo Paquet Glynn Winskel
The concurrent game semantics of Probabilistic PCFMore Information... - Yijia Chen Jörg Flum
Tree-depth, quantifier elimination, and quantifier rankMore Information... - Yijia Chen Moritz Müller Keita Yokoyama
A parameterized halting problem, the linear time hierarchy, and the MRDP theoremMore Information... - Thierry Coquand Simon Huber Anders Mörtberg
On Higher Inductive Types in Cubical Type TheoryMore Information... - Karl Crary
Strong Sums in Focused LogicMore Information... - Raphaëlle Crubillé
Probabilistic Stable Functions on Discrete Cones are Power SeriesMore Information... - Daniel Danielski Emanuel Kieronski
Unary negation fragment with equivalence relations has the finite model propertyMore Information... - Luc Dartois Emmanuel Filiot Nathan Lhote
Logics for Word Transductions with SynthesisMore Information... - Ankush Das Jan Hoffmann Frank Pfenning
Work Analysis with Resource-Aware Session TypesMore Information... - Vrunda Dave Paul Gastin Shankara Narayanan Krishna
Regular Transducer Expressions for Regular TransformationsMore Information... - Laure Daviaud Marcin Jurdzinski Ranko Lazic
A pseudo-quasi-polynomial algorithm for mean-payoff parity gamesMore Information... - Romain Demangeon Nobuko Yoshida
Causal Computational Complexity of Distributed ProcessesMore Information... - Arnaud Durand Anselm Haak Heribert Vollmer
Model-Theoretic Characterization of Boolean and Arithmetic Circuit Classes of Small DepthMore Information... - Adrien Durier Daniel Hirschkoff Davide Sangiorgi
Eager Functions as ProcessesMore Information... - Clovis Eberhart Tom Hirschowitz
What's in a game?: A theory of game modelsMore Information... - Javier Esparza Jan Kretínský Salomon Sickert
One Theorem to Rule Them All: A Unified Translation of LTL into ω-AutomataMore Information... - Thomas Ferrère Thomas A. Henzinger N. Ege Saraç
A Theory of Register MonitorsMore Information... - Diego Figueira M. Praveen
Playing with Repetitions in Data Words Using Energy GamesMore Information... - Nathanaël Fijalkow
The State Complexity of Alternating AutomataMore Information... - Emmanuel Filiot Raffaella Gentilini Jean-François Raskin
Rational Synthesis Under Imperfect InformationMore Information... - Dror Fried Axel Legay Joël Ouaknine Moshe Y. Vardi
Sequential Relational DecompositionMore Information... - Dan Frumin Robbert Krebbers Lars Birkedal
ReLoC: A Mechanised Relational Logic for Fine-Grained ConcurrencyMore Information... - Francesco Gavazzo
Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative DistancesMore Information... - Guillaume Geoffroy
Classical realizability as a classifier for nondeterminismMore Information... - Neil Ghani Jules Hedges Viktor Winschel Philipp Zahn
Compositional Game TheoryMore Information... - Grzegorz Gluch Jerzy Marcinkowski Piotr Ostropolski-Nalewaja
Can One Escape Red Chains?: Regular Path Queries Determinacy is UndecidableMore Information... - Adrien Guatto
A Generalized Modality for RecursionMore Information... - Amar Hadzihasanovic Kang Feng Ng Quanlong Wang
Two complete axiomatisations of pure-state qubit quantum computingMore Information... - Michael Hahn Andreas Krebs Howard Straubing
Wreath Products of Distributive Forest AlgebrasMore Information... - Ross Horne Ki Yung Ahn Shang-Wei Lin Alwen Tiu
Quasi-Open Bisimilarity with Mismatch is IntuitionisticMore Information... - Ehud Hrushovski Joël Ouaknine Amaury Pouly James Worrell
Polynomial Invariants for Affine ProgramsMore Information... - Dominic J. D. Hughes
Unification nets: canonical proof net quantifiersMore Information... - Pawel M. Idziak Jacek Krzaczkowski
Satisfiability in multi-valued circuitsMore Information... - Emmanuel Jeandel Simon Perdrix Renaud Vilmart
A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum MechanicsMore Information... - Emmanuel Jeandel Simon Perdrix Renaud Vilmart
Diagrammatic Reasoning beyond Clifford+T Quantum MechanicsMore Information... - Bruce M. Kapron Florian Steinberg
Type-two polynomial-time and restricted lookaheadMore Information... - Marie Kerjean
A Logical Account for Linear Partial Differential EquationsMore Information... - Nicolai Kraus Thorsten Altenkirch
Free Higher Groups in Homotopy Type TheoryMore Information... - Jan Kretínský Tobias Meggendorfer
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision ProcessesMore Information... - Antti Kuusisto Carsten Lutz
Weighted model counting beyond two-variable logicMore Information... - Olivier Laurent
Around Classical and Intuitionistic Linear LogicsMore Information... - Karoliina Lehtinen
A modal μ perspective on solving parity games in quasi-polynomial timeMore Information... - Thomas Leventis
Probabilistic Böhm Trees and Probabilistic SeparationMore Information... - Bert Lindenhovius Michael Mislove Vladimir Zamdzhiev
Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String DiagramsMore Information... - Paul-André Melliès
Ribbon Tensorial LogicMore Information... - Paul-André Melliès Léo Stefanesco
An Asynchronous Soundness Theorem for Concurrent Separation LogicMore Information... - Matteo Mio
Riesz Modal Logic with Threshold OperatorsMore Information... - Étienne Miquey
A sequent calculus with dependent types for classical arithmeticMore Information... - Benoit Monin
An answer to the Gamma questionMore Information... - Sean K. Moss Tamara von Glehn
Dialectica models of type theoryMore Information... - Koko Muroya Steven W. T. Cheung Dan R. Ghica
The Geometry of Computation-Graph AbstractionMore Information... - Yoji Nanjo Hiroshi Unno Eric Koskinen Tachio Terauchi
A Fixpoint Logic and Dependent Effects for Temporal Property VerificationMore Information... - Matthias Niewerth
MSO Queries on Trees: Enumerating Answers under Updates Using Forest AlgebrasMore Information... - Andreas Nuyts Dominique Devriese
Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type TheoryMore Information... - Michal Pilipczuk Sebastian Siebertz Szymon Torunczyk
Parameterized circuit complexity of model-checking on sparse structuresMore Information... - Michal Pilipczuk Sebastian Siebertz Szymon Torunczyk
On the number of types in sparse graphsMore Information... - Maciej Piróg Tom Schrijvers Nicolas Wu Mauro Jaskelioff
Syntax and Semantics for Operations with ScopesMore Information... - André Platzer Yong Kiam Tan
Differential Equation Axiomatization: The Impressive Power of Differential GhostsMore Information... - Damien Pous Valeria Vignudelli
Allegories: decidability and graph homomorphismsMore Information... - Thomas Powell
A functional interpretation with stateMore Information... - Pierre Pradic Colin Riba
LMSO: A Curry-Howard Approach to Church's Synthesis via Linear LogicMore Information... - Benjamin Sherman Luke Sciarappa Adam Chlipala Michael Carbin
Computable decision making on the reals and other spaces: via partiality and nondeterminismMore Information... - Nadish de Silva
Logical paradoxes in quantum computationMore Information... - Kristina Sojakova Patricia Johann
A General Framework for Relational ParametricityMore Information... - Jonathan Sterling Robert Harper
Guarded Computational Type TheoryMore Information... - Takeshi Tsukada Kazuyuki Asada C.-H. Luke Ong
Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum ProgramsMore Information... - Pierre Vial
Every λ-Term is Meaningful for the Infinitary Relational ModelMore Information... - Paul Wild Lutz Schröder Dirk Pattinson Barbara König
A van Benthem Theorem for Fuzzy Modal LogicMore Information... - Noam Zeilberger
A theory of linear typings as flows on 3-valent graphsMore Information... - Georg Zetzsche
Separability by piecewise testable languages and downward closures beyond subwordsMore Information...
Organizers
General ChairMartin Grohe Program ChairMartin Hofmann Conference ChairSam Staton Publicity ChairSam Staton Workshops ChairPatricia Bouyer |
Program Committee:Gilles Barthe (IMDEA Software Institute); Michael Benedikt (Univ. Oxford); Hans L. Bodlaender (Utrecht University); Ugo Dal Lago (Univ. Bologna & INRIA Sophia Antipolis); Samir Datta (Chennai Mathematical Institute); Anuj Dawar (Univ. Cambridge); Josee Desharnais (Univ. Laval); Jerome Feret (INRIA, ENS Paris); Erich Grädel (RWTH Aachen); Ichiro Hasuo (NII Tokyo); Justin Hsu (UCL); Alan Jeffrey (Mozilla Research); Bartek Klin (Univ. Warsaw); Antonina Kolokolova (Memorial Univ. Newfoundland); Orna Kupferman (Hebrew Univ. Jerusalem); Daniel Leivant (Indiana Univ.); Daniel R. Licata (Carnegie Mellon University); Anthony Widjaja Lin (Univ. Oxford); Sebastian Maneth (Univ. Bremen); Anca Muscholl (Univ. Bordeaux); Brigitte Pientka (McGill University); Thomas Place (Univ. Bordeaux); Ramyaa Ramyaa (New Mexico Tech.); Giselle Reis (Carnegie Mellon (Qatar)); Sylvain Schmitz (ENS Paris-Saclay); Nicole Schweikardt (HU Berlin); Peter Selinger (Dalhousie University); Zhong Shao (Yale University); Ana Sokolova (Univ. Salzburg); Thomas Streicher (TU Darmstadt); Carolyn Talcott (SRI International); Lijun Zhang (Chinese Academy of Sciences, Beijing) |