


default search action
33rd LICS 2018: Oxford, UK
- Anuj Dawar, Erich Grädel:

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. ACM 2018 - Michael Blondin

, Javier Esparza
, Stefan Jaax, Antonín Kucera
:
Black Ninjas in the Dark: Formal Analysis of Population Protocols. 1-10 - Thierry Coquand:

Inner Models of Univalence. 11-12 - Peter W. O'Hearn:

Continuous Reasoning: Scaling the impact of formal methods. 13-25 - Ross Horne

, Ki Yung Ahn, Shang-Wei Lin
, Alwen Tiu:
Quasi-Open Bisimilarity with Mismatch is Intuitionistic. 26-35 - S. Akshay, Blaise Genest, Nikhil Vyas:

Distribution-based objectives for Markov Decision Processes. 36-45 - Joël D. Allred

, Ulrich Ultes-Nitsche
:
A Simple and Optimal Complementation Algorithm for Büchi Automata. 46-55 - Robert Atkey:

Syntax and Semantics of Quantitative Type Theory. 56-65 - Albert Atserias, Joanna Ochremiak:

Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem. 66-75 - Steve Awodey, Jonas Frey

, Sam Speight
:
Impredicative Encodings of (Higher) Inductive Types. 76-85 - Christel Baier

, Nathalie Bertrand
, Clemens Dubslaff, Daniel Gburek, Ocan Sankur:
Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes. 86-94 - Valentin Blot, Jim Laird

:
Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types. 95-104 - Manuel Bodirsky

, Florent R. Madelaine
, Antoine Mottet:
A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP. 105-114 - Rose Bohrer

, André Platzer
:
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow. 115-124 - Mikolaj Bojanczyk, Laure Daviaud

, Shankara Narayanan Krishna:
Regular and First-Order List Functions. 125-134 - Mikolaj Bojanczyk, Martin Grohe, Michal Pilipczuk

:
Definable decompositions for graphs of bounded linear cliquewidth. 135-144 - Mikolaj Bojanczyk, Szymon Torunczyk

:
On computability and tractability for infinite sets. 145-154 - Udi Boker, Yariv Shaulian:

Automaton-Based Criteria for Membership in CTL. 155-164 - Filippo Bonchi

, Fabio Gadducci
, Aleks Kissinger
, Pawel Sobocinski
, Fabio Zanasi
:
Rewriting with Frobenius. 165-174 - Filippo Bonchi

, Pierre Ganty, Roberto Giacobazzi, Dusko Pavlovic
:
Sound up-to techniques and Complete abstract domains. 175-184 - Tomás Brázdil, Krishnendu Chatterjee

, Antonín Kucera
, Petr Novotný
, Dominik Velan, Florian Zuleger
:
Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. 185-194 - Roberto Bruni, Hernán C. Melgratti, Ugo Montanari:

Concurrency and Probability: Removing Confusion, Compositionally. 195-204 - Ulrik Buchholtz

, Floris van Doorn, Egbert Rijke:
Higher Groups in Homotopy Type Theory. 205-214 - Simon Castellan, Pierre Clairambault, Hugo Paquet, Glynn Winskel:

The concurrent game semantics of Probabilistic PCF. 215-224 - Yijia Chen, Jörg Flum:

Tree-depth, quantifier elimination, and quantifier rank. 225-234 - Yijia Chen, Moritz Müller, Keita Yokoyama

:
A parameterized halting problem, the linear time hierarchy, and the MRDP theorem. 235-244 - Mark Bickford, Liron Cohen

, Robert L. Constable, Vincent Rahli
:
Computability Beyond Church-Turing via Choice Sequences. 245-254 - Thierry Coquand, Simon Huber, Anders Mörtberg:

On Higher Inductive Types in Cubical Type Theory. 255-264 - Karl Crary:

Strong Sums in Focused Logic. 265-274 - Raphaëlle Crubillé:

Probabilistic Stable Functions on Discrete Cones are Power Series. 275-284 - Daniel Danielski

, Emanuel Kieronski
:
Unary negation fragment with equivalence relations has the finite model property. 285-294 - Luc Dartois

, Emmanuel Filiot
, Nathan Lhote:
Logics for Word Transductions with Synthesis. 295-304 - Ankush Das

, Jan Hoffmann, Frank Pfenning:
Work Analysis with Resource-Aware Session Types. 305-314 - Vrunda Dave, Paul Gastin, Shankara Narayanan Krishna:

Regular Transducer Expressions for Regular Transformations. 315-324 - Laure Daviaud

, Marcin Jurdzinski
, Ranko Lazic:
A pseudo-quasi-polynomial algorithm for mean-payoff parity games. 325-334 - Nadish de Silva:

Logical paradoxes in quantum computation. 335-343 - Romain Demangeon, Nobuko Yoshida

:
Causal Computational Complexity of Distributed Processes. 344-353 - Arnaud Durand, Anselm Haak, Heribert Vollmer

:
Model-Theoretic Characterization of Boolean and Arithmetic Circuit Classes of Small Depth. 354-363 - Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi:

Eager Functions as Processes. 364-373 - Clovis Eberhart

, Tom Hirschowitz
:
What's in a game?: A theory of game models. 374-383 - Javier Esparza

, Jan Kretínský, Salomon Sickert:
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. 384-393 - Thomas Ferrère, Thomas A. Henzinger, N. Ege Saraç

:
A Theory of Register Monitors. 394-403 - Diego Figueira

, M. Praveen:
Playing with Repetitions in Data Words Using Energy Games. 404-413 - Nathanaël Fijalkow

:
The State Complexity of Alternating Automata. 414-421 - Emmanuel Filiot

, Raffaella Gentilini, Jean-François Raskin:
Rational Synthesis Under Imperfect Information. 422-431 - Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi:

Sequential Relational Decomposition. 432-441 - Dan Frumin

, Robbert Krebbers, Lars Birkedal
:
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. 442-451 - Francesco Gavazzo

:
Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances. 452-461 - Guillaume Geoffroy

:
Classical realizability as a classifier for nondeterminism. 462-471 - Neil Ghani, Jules Hedges, Viktor Winschel, Philipp Zahn:

Compositional Game Theory. 472-481 - Adrien Guatto:

A Generalized Modality for Recursion. 482-491 - Grzegorz Gluch, Jerzy Marcinkowski

, Piotr Ostropolski-Nalewaja
:
Can One Escape Red Chains?: Regular Path Queries Determinacy is Undecidable. 492-501 - Amar Hadzihasanovic

, Kang Feng Ng, Quanlong Wang:
Two complete axiomatisations of pure-state qubit quantum computing. 502-511 - Michael Hahn, Andreas Krebs, Howard Straubing:

Wreath Products of Distributive Forest Algebras. 512-520 - Ulrik Buchholtz

, Kuen-Bang Hou (Favonia):
Cellular Cohomology in Homotopy Type Theory. 521-529 - Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, James Worrell

:
Polynomial Invariants for Affine Programs. 530-539 - Dominic J. D. Hughes:

Unification nets: canonical proof net quantifiers. 540-549 - Pawel M. Idziak, Jacek Krzaczkowski

:
Satisfiability in multi-valued circuits. 550-558 - Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart:

A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics. 559-568 - Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart:

Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics. 569-578 - Bruce M. Kapron

, Florian Steinberg:
Type-two polynomial-time and restricted lookahead. 579-588 - Marie Kerjean

:
A Logical Account for Linear Partial Differential Equations. 589-598 - Nicolai Kraus

, Thorsten Altenkirch:
Free Higher Groups in Homotopy Type Theory. 599-608 - Jan Kretínský, Tobias Meggendorfer

:
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes. 609-618 - Antti Kuusisto

, Carsten Lutz:
Weighted model counting beyond two-variable logic. 619-628 - Olivier Laurent:

Around Classical and Intuitionistic Linear Logics. 629-638 - Karoliina Lehtinen

:
A modal μ perspective on solving parity games in quasi-polynomial time. 639-648 - Thomas Leventis:

Probabilistic Böhm Trees and Probabilistic Separation. 649-658 - Bert Lindenhovius

, Michael W. Mislove
, Vladimir Zamdzhiev
:
Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams. 659-668 - Giorgio Bacci

, Robert Furber
, Dexter Kozen, Radu Mardare, Prakash Panangaden, Dana S. Scott:
Boolean-Valued Semantics for the Stochastic λ-Calculus. 669-678 - Giorgio Bacci

, Radu Mardare, Prakash Panangaden, Gordon D. Plotkin:
An Algebraic Theory of Markov Processes. 679-688 - Paul-André Melliès

:
Ribbon Tensorial Logic. 689-698 - Paul-André Melliès, Léo Stefanesco:

An Asynchronous Soundness Theorem for Concurrent Separation Logic. 699-708 - Matteo Mio:

Riesz Modal Logic with Threshold Operators. 710-719 - Étienne Miquey

:
A sequent calculus with dependent types for classical arithmetic. 720-729 - Benoit Monin:

An answer to the Gamma question. 730-738 - Sean K. Moss, Tamara von Glehn:

Dialectica models of type theory. 739-748 - Koko Muroya, Steven W. T. Cheung, Dan R. Ghica:

The Geometry of Computation-Graph Abstraction. 749-758 - Yoji Nanjo, Hiroshi Unno

, Eric Koskinen, Tachio Terauchi
:
A Fixpoint Logic and Dependent Effects for Temporal Property Verification. 759-768 - Matthias Niewerth:

MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras. 769-778 - Andreas Nuyts

, Dominique Devriese
:
Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory. 779-788 - Michal Pilipczuk

, Sebastian Siebertz
, Szymon Torunczyk
:
Parameterized circuit complexity of model-checking on sparse structures. 789-798 - Michal Pilipczuk

, Sebastian Siebertz
, Szymon Torunczyk
:
On the number of types in sparse graphs. 799-808 - Maciej Piróg

, Tom Schrijvers
, Nicolas Wu
, Mauro Jaskelioff:
Syntax and Semantics for Operations with Scopes. 809-818 - André Platzer

, Yong Kiam Tan:
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. 819-828 - Damien Pous, Valeria Vignudelli:

Allegories: decidability and graph homomorphisms. 829-838 - Thomas Powell

:
A functional interpretation with state. 839-848 - Cécilia Pradic, Colin Riba:

LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic. 849-858 - Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin:

Computable decision making on the reals and other spaces: via partiality and nondeterminism. 859-868 - Kristina Sojakova, Patricia Johann:

A General Framework for Relational Parametricity. 869-878 - Jonathan Sterling

, Robert Harper:
Guarded Computational Type Theory. 879-888 - 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 Programs. 889-898 - Pierre Vial:

Every λ-Term is Meaningful for the Infinitary Relational Model. 899-908 - Paul Wild, Lutz Schröder

, Dirk Pattinson, Barbara König:
A van Benthem Theorem for Fuzzy Modal Logic. 909-918 - Noam Zeilberger

:
A theory of linear typings as flows on 3-valent graphs. 919-928 - Georg Zetzsche

:
Separability by piecewise testable languages and downward closures beyond subwords. 929-938

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














