yusuke1997/dblp-id-title huggingface dataset:
Undecidability of Propositional Separation Logic and Its Neighbours
Algebraic Approach to Approximation
A Characterisation Theorem for Two-Way Bisimulation-Invariant Monadic Least Fixpoint Logic Over Finite Structures
Feasible Proofs and Computations: Partnership and Fusion
Stratified Bounded Affine Logic for Logarithmic Space
Modal Characterisation Theorems over Special Classes of Frames
Computing Unification Algorithms
On the Query Complexity of Real Functionals
17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings
A Cartesian Closed Category for Random Variables
Computational Complexity of Some Problems Involving Congruences on Algebras
Recognisability Equals Definability for Finitely Representable Matroids of Bounded Path-Width
A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams
Computational Complexity of Quantum Satisfiability
Spectrum Hierarchies and Subdiagonal Functions
The Weisfeiler-Leman dimension of planar graphs is at most 3
A Non-Type-Theoretic Definition of Martin-Löf's Types
Solving Partial-Information Stochastic Parity Games
Inner Models of Univalence
Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996
Parikh's theorem for infinite alphabets
An Improved Algorithm for the Automatic Verification of Finite State Systems Using Temporal Logic
Strong Complementarity and Non-locality in Categorical Quantum Mechanics
First order distinguishability of sparse random graphs
Revisiting Digitization, Robustness, and Decidability for Timed Automata
0-1 Laws for Infinitary Logics (Preliminary Report)
An Evaluation Semantics for Classical Proofs
The Type and Effect Discipline
A Complete Logical Calculus for Record Structures Representing Linguistic Information
Quantifier Free Definability on Infinite Algebras
Approximate Pattern Matching is Expressible in Transitive Closure Logic
From Automata to Formulas: Convex Integer Polyhedra
Two-Variable Logic with Counting and Trees
On Digraph Coloring Problems and Treewidth Duality
Generalized Quantifiers and Pebble Games on Finite Structures
Strong Normalization for System F by HOAS on Top of FOAS
A Cellular Howe Theorem
Managing Digital Rights using Linear Logic
Static Name Control for FreshML
Mechanizing the Metatheory of LF
The Theory of Ground Rewrite Systems is Decidable
Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
Parallel PCF Has a Unique Extensional Model
Effective Domains and Intrinsic Structure
Model-Checking Problems as a Basis for Parameterized Intractability
Reasoning about Local Variables with Operationally-Based Logical Relations
Extended Kripke lemma and decidability for hypersequent substructural logics
Paramodulation with Non-Monotonic Orderings
Naturality for higher-dimensional path types
Dependent Intersection: A New Way of Defining Records in Type Theory
LTL with the Freeze Quantifier and Register Automata
Abstracting the Differential Semantics of Rule-Based Models: Exact and Automated Model Reduction
A Timely Resolution
An interpretation of system F through bar recursion
Asynchronous Communication in Process Algebra
Minimal Taylor Algebras as a Common Framework for the Three Algebraic Approaches to the CSP
38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023
Programs for Cheap!
Recursive Types in Games: Axiomatics and Process Representation
Freyd's Hierarchy of Combinator Monoids
A Logic of Subtyping (Extended Abstract)
A Note on the Complexity of Classical and Intuitionistic Proofs
Wreath Products of Forest Algebras, with Applications to Tree Logics
The Power of Arc Consistency for CSPs Defined by Partially-Ordered Forbidden Patterns
Uniform, integral and efficient proofs for the determinant identities
Fragments of Existential Second-Order Logic without 0-1 Laws
Determinisation and Unambiguisation of Polynomially-Ambiguous Rational Weighted Automata
Boolean Algebras for Lambda Calculus
The Mathematics of Nonmonotonic Reasoning (Abstract)
Petri Nets Are Monoids: A New Algebraic Foundation for Net Theory
A Stratified Semantics of General References A Stratified Semantics of General References
Propositional Proof Complexity: A Survey on the State of the Art, Including Some Recent Results
Models for Name-Passing Processes: Interleaving and Causal
Rational Synthesis Under Imperfect Information
I'm OK if You're OK: On the Notion of Trusting Communication
Monomial size vs. Bit-complexity in Sums-of-Squares and Polynomial Calculus
A Coinduction Principle for Recursive Data Types Based on Bisimulation
A pseudo-quasi-polynomial algorithm for mean-payoff parity games
Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods
Dominator Trees and Fast Verification of Proof Nets
On the Ordered Conjecture
Symbolic execution and probabilistic reasoning
On The Lambda Y Calculus
Automatic Structures: Twenty Years Later
The Probabilistic Model Checking Landscape
When is Ontology-Mediated Querying Efficient?
Minimization of Symbolic Tree Automata
Model-Checking of Causality Properties
Learning Deterministic One-Counter Automata in Polynomial Time
Game Semantics for a Polymorphic Programming Language
Resource approximation for the λμ-calculus
Constructive Negation for Constraint Logic Programming
The Nonexistence of Finite Axiomatisations for CCS Congruences
Stone Duality for Markov Processes
Calculus in Coinductive Form
An Observationally Complete Program Logic for Imperative Higher-Order Frame Rules
My 27-year Quest to Overcome the State Explosion Problem
Descriptive Complexity of List H-Coloring Problems in Logspace: A Refined Dichotomy
Extensions of Domain Maps in Differential and Integral Calculus
Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science
Verification of Concurrent Programs: The Automata-Theoretic Framework
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
Monoidal Streams for Dataflow Programming
Axiomatizations and Computability of Weighted Monadic Second-Order Logic
Kripke Semantics for Modal Bilattice Logic
How unprovable is Rabin's decidability theorem?
A Logic for Reasoning about Probabilities
Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable
Positive First-order Logic on Words
The Identity Problem in virtually solvable matrix groups over algebraic numbers
Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions
Typing and Subtyping for Mobile Processes
Labelled Markov Processes: Stronger and Faster Approximations
From Finite-Valued Nondeterministic Transducers to Deterministic Two-Tape Automata
Merging Functional with Relational Programming in a Reduction Setting (Abstract of an Invited Lecture)
Computing the linear hull: Deciding Deterministic? and Unambiguous? for weighted automata over fields
Uniform Proofs and Disjunctive Logic Programming (Extended Abstract)
Random Worlds and Maximum Entropy
A Complete Axiomatisation for Divergence Preserving Branching Congruence of Finite-State Behaviours
Work Analysis with Resource-Aware Session Types
Minimal Model Semantics for Nonmonotonic Modal Logics
Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction
Reasoning with Many Processes
A Choppy Logic
Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory
Fixpoint Extensions of First-Order Logic and Datalog-Like Languages
A Robust Class of Context-Sensitive Languages
Extensional Equality in Intensional Type Theory
Understanding Gentzen and Frege Systems for QBF
Infinitary Logics and Very Sparse Random Graphs
15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000
Temporal Logics and Model Checking for Fairly Correct Systems
Independence and Concurrent Separation Logic
The sorrows of a smooth digraph: the first hardness criterion for infinite directed graph-colouring problems
Approximate Evaluation of Quantitative Second Order Queries
Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects
Mean-Payoff Parity Games
The Essence of Parallel Algol
Universal equivalence and majority of probabilistic programs over finite fields
Homomorphism Closed vs. Existential Positive
An Intuitionistic Logic that Proves Markov's Principle
An abstract standardisation theorem
Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), Montreal, Canada, June 19-23, 1993
Proving Termination Properties of Prolog Programs: A Semantic Approach
Logic in Software, Dynamical and Biological Systems
Logical Step-Indexed Logical Relations
Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes
14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999
Proof Nets for Additive Linear Logic with Units
Polynomial automata: Zeroness and applications
A Computational Analysis of Girard's Translation and LC
A Generic Operational Metatheory for Algebraic Effects
Boolean symmetric vs. functional PCSP dichotomy
A New Approach to Abstract Syntax Involving Binders
Proof Techniques for Cryptographic Processes
First Order Formulas with Modular Predicates
Topology is relevant (in a dichotomy conjecture for infinite-domain constraint satisfaction problems)
Algorithmic barriers to representing conditional independence
Algorithm Development in the Calculus of Constructions
Operational Algorithmic Game Semantics
Learning first-order definable concepts over structures of small degree
"Upon This Quote I Will Build My Church Thesis"
Complete Sequent Calculi for Induction and Infinite Descent
Cyclic Implicit Complexity
Higher Lenses
Temporal Logic with Forgettable Past
Relating Word and Tree Automata
Proceedings of the Workshop on Logical Aspects of Fault Tolerance, LAFT@LICS 2009, Los Angeles, CA, USA, August 15, 2009
Separation and Encodability in Mixed Choice Multiparty Sessions
On the Geometry of Interaction for Classical Logic
Logically Presented Domains
Regular Repair of Specifications
On the Scope of the Universal-Algebraic Approach to Constraint Satisfaction
Order-Sorted Algebra solves the Constructor-Selector, Multiple
A Compositional Proof System for Dynamic Process Creation
Safety and Liveness in Branching Time
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
On Probabilistic Automata in Continuous Time
Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads
Model Comparison Games for Horn Description Logics
Curry and Howard Meet Borel
From the Church-Turing Thesis to the First-Order Algorithm Theorem
L. E. J. Brouwer's Intuitionism: A Revolution in Two Installments
Complexity Transfer for Modal Logic (Extended Abstract)
Winning Cores in Parity Games
A Categorical Semantics of Quantum Protocols
Theorem Proving for Verification: The Early Days
Minimization of Dynamical Systems over Monoids
MSO+∇ is undecidable
Reasoning about Data Repetitions with Counter Systems
Expressive Equivalence of Least and Inflationary Fixed-Point Logic
Large scale geometries of infinite strings
Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games
Denotational semantics of recursive types in synthetic guarded domain theory
Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), Santa Cruz, California, USA, June 22-25, 1992
An expressively complete local past propositional dynamic logic over Mazurkiewicz traces and its applications
Definability of semidefinite programming and lasserre lower bounds for CSPs
The Genericity Theorem and the Notion of Parametricity in the Polymorphic lambda-calculus (Extended Abstract)
Positional ω-regular languages
Three Logics for Branching Bisimulation (Extended Abstract)
Equality between Functionals in the Presence of Coproducts
An answer to the Gamma question
A Generic Normal Form for ZX-Diagrams and Application to the Rational Angle Completeness
Living without Beth and Craig: Definitions and Interpolants in the Guarded and Two-Variable Fragments
On the Boundedness Problem for Two-Variable First-Order Logic
Modelling Computations: A 2-Categorical Framework
Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory
The Hunt for a Red Spider: Conjunctive Query Determinacy Is Undecidable
Complete Graphical Language for Hermiticity-Preserving Superoperators
The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens
Feedback Turing Computability, and Turing Computability as Feedback
mu-Definable Sets of Integers
Reasoning on Data Words over Numeric Domains
Foundations of information integration under bag semantics
Definability on a Random 3-CNF Formula
Template games and differential linear logic
A Calculus of Dataflow Networks (Extended Abstract)
Pi-Calculus in Logical Form
Regular Real Analysis
Coinduction All the Way Up
Noncomputable Conditional Distributions
Constraint satisfaction problems over semilattice block Mal'tsev algebras
Testing, Optimizaton, and Games
Reactive, Generative, and Stratified Models of Probabilistic Processes
The Fixed Point Property in Synthetic Domain Theory
Infinitary intersection types as sequences: A new answer to Klop's problem
Non-trivial Power Types Can't Be Subtypes of Polymorphic Types
A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation
LICS: Logic in Computer Security - Some Attacker's Models and Related Decision Problems
Flipping and Forking
Proving Termination Assertions in Dynamic Logics
Local normal forms and their use in algorithmic meta theorems (Invited Talk)
A Compositional Proof System for the Modal mu-Calculus
A Theory of Recursive Domains with Applications to Concurrency
On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study
Logics of Dynamical Systems
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
Query Evaluation on Compressed Trees (Extended Abstract)
Why is it Hard to Obtain a Dichotomy for Consistent Query Answering?
Context Semantics, Linear Logic and Computational Complexity
Double-exponential Complexity of Computing a Complete Set of AC-Unifiers
Proving Boolean Combinations of Deterministic Properties
On the Context-Freeness Problem for Vector Addition Systems
Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering
Proof Compression via Subatomic Logic and Guarded Substitutions
Bisimilarity in Fresh-Register Automata
A Category of Labelled Petri Nets and Compositional Proof System (Extended Abstract)
Elf: A Language for Logic Definition and Verified Metaprogramming
Matching Explicit and Modal Reasoning about Programs: A Proof Theoretic Delineation of Dynamic Logic
Computing Optimal Coverability Costs in Priced Timed Petri Nets
Concurrent Games over Relational Structures: The Origin of Game Comonads
Relations in Concurrency
On First-Order Topological Queries
Structure and Representation in LF
The Relation Between Second-Order Unification and Simultaneous Rigid E -Unification
On Simultaneously Determinizing and Complementing omega-Automata (Extended Abstract)
Extensional and Non-extensional Functions as Processes
Efficient Construction of Reversible Transducers from Regular Transducer Expressions
Some Decision Problems of Enormous Complexity
Combinatorial Proofs and Decomposition Theorems for First-order Logic
Bisimulation: From The Origins to Today
Proving Security Protocols Correct
Relevance Logic and Concurrent Composition
The Smash Product of Monoidal Theories
On the Power of Bounded Concurrency~III: Reasoning About Programs (Preliminary Report)
On the Expressive Power of Homomorphism Counts
An Algebraic Model of Parallel Execution of Logic Programs
A direct computational interpretation of second-order arithmetic via update recursion
Good-for-games ω-Pushdown Automata
Logics for Word Transductions with Synthesis
Imperative Programming with Dependent Types
The Hierarchy inside Closed Monadic Sigma 1 Collapses on the Infinite Binary Tree
Some Strategies for Proving Theorems with a Model Checker
Game Semantics & Abstract Machines
Separating Rank Logic from Polynomial Time
The Complexity of Reachability in Affine Vector Addition Systems with States
Automata on the Integers, Recurrence Distinguishability, and the Equivalence and Decidability of Monadic Theories
Recursive Types and Type Constraints in Second-Order Lambda Calculus
Coproducts of Monads on Set
Sequentiality, Second Order Monadic Logic and Tree Automata
First-Order Logic vs. Fixed-Point Logic in Finite Set Theory
X-Separability and Left-Invertibility in lambda-calculus
On Counting Logics and Local Properties
On the complexity of Maslov's class K
Compositional Verification of Real-Time Systems
Ground Reducibility is EXPTIME-Complete
The Topological Mu-Calculus: completeness and decidability
Proof-Theoretic Techniques for Term Rewriting Theory
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Partial-Order Methods for Model Checking: From Linear Time to Branching Time
Equation Solving Using Modal Transition Systems
The Topology of Program Termination
Effectful Mealy Machines: Bisimulation and Trace
A Constructive Proof of Higman's Lemma
Consuming and Persistent Types for Classical Logic
Semantical Analysis of Intuitionistic Modal Logics between CK and IK
Automatic Amortized Resource Analysis with Regular Recursive Types
The Descriptive Complexity of Graph Neural Networks
The Stone Gamut: A Coordinatization of Mathematics
Proving Differential Privacy via Probabilistic Couplings
Promises Make Finite (Constraint Satisfaction) Problems Infinitary
The Infinitary Logic of Sparse Random Graphs
Back and Forth between Guarded and Modal Logics
The Undecidability of Boolean BI through Phase Semantics
DATALOG SIRUPs Uniform Boundedness is Undecidable
Theorem Proving Using Rigid E-Unification Equational Matings
Compositional relational reasoning via operational game semantics
Correctness of Multiplicative Additive Proof Structures is NL-Complete
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
Intuitionistic proofs without syntax
Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract)
Linear Types, Approximation, and Topology
Indexed Containers
Monadic Chain Logic Over Iterations and Applications to Pushdown Systems
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs
Model Checking Vs. Generalized Model Checking: Semantic Minimizations for Temporal Logics
Converging to the Chase - A Tool for Finite Controllability
The Blurred Drinker Paradox: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem
Cyclic Lambda Graph Rewriting
Backprop as Functor: A compositional perspective on supervised learning
Game Semantics for Type Soundness
Logics with Counting, Auxiliary Relations, and Lower Bounds for Invariant Queries
A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation
Rewriting modulo symmetric monoidal structure
Effective Brenier Theorem: Applications to Computable Analysis and Algorithmic Randomness
On the Growth Rates of Polyregular Functions
Zero-One Laws for Gilbert Random Graphs
Definability and Compression
Distinguishing Hidden Markov Chains
Concurrent Strategies
Nested Weighted Automata
The Yoneda embedding in simplicial type theory
Succinct progress measures for solving parity games
Commutative Monads for Probabilistic Programming Languages
A Static Calculus of Dependencies for the lambda-Cube
A monad for full ground reference cells
Bisimulation and Co-induction (Tutorial)
An Algebraic Characterisation of First-Order Logic with Neighbour
On the Computational Complexity of Verifying One-Counter Processes
On the Separability Problem of VASS Reachability Languages
A cartesian-closed category for higher-order model checking
Cut Elimination for Monomial MALL Proof Nets
On Generalized Metric Spaces for the Simply Typed Lambda-Calculus
Structural Cut Elimination
Combining fixpoint and differentiation theory
Choiceless Polynomial Time with Witnessed Symmetric Choice
Discounted-Sum Automata with Real-Valued Discount Factors
Decidability and Complexity for Quiescent Consistency
A Stability Theorem in Rewriting Theory
Semantics and Logic of Object Calculi
Privacy, Anonymity, and Accountability in Ad-Supported Services
Name Generation and Linearity
Game Relations and Metrics
Resolving finite indeterminacy: A definitive constructive universal prime ideal theorem
A Fixpoint Logic and Dependent Effects for Temporal Property Verification
Delta-Decidability over the Reals
Petri Automata for Kleene Allegories
Complete Problems for Dynamic Complexity Classes
On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees
Standard ML-NJ weak polymorphism and imperative constructs
The Inverse Taylor Expansion Problem in Linear Logic
On the Computational Power of Universally Polymorphic Recursion
A Foundational Delineation of Computational Feasiblity
Complete Proof Systems for First Order Interval Temporal Logic
Asynchronous Extensions of HyperLTL
Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives
Third Order Matching is Decidable
The notion of a Framework and a framework for LTC
3D-grids are not transducible from planar graphs
A Superposition Decision Procedure for the Guarded Fragment with Equality
From Complexity to Algebra and Back: Digraph Classes, Collapsibility, and the PGP
Verifying Programs with Unreliable Channels
The Subtyping Problem for Second-Order Types is Undecidable
Maltsev + Datalog --> Symmetric Datalog
Games Semantics for Full Propositional Linear Logic
Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps
Making Streett Determinization Tight
A Symbolic Labelled Transition System for Coinductive Subtyping of F µ< Types
Partial Univalence in n-truncated Type Theory
A Kleene Theorem for Timed Automata
PDL Is the Bisimulation-Invariant Fragment of Weak Chain Logic
Where First-Order and Monadic Second-Order Logic Coincide
Operational aspects of linear lambda calculus
Zigzag normalisation for associative n-categories
A Decision Procedure for an Extensional Theory of Arrays
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements
Quantitative and Approximate Monitoring
A Type System for Complexity Flow Analysis
Datalog+/-: A Family of Logical Knowledge Representation and Query Languages for New Applications
Semantic Parametricity in Polymorphic Lambda Calculus
Von Neumann's Biased Coin Revisited
Type Inference for Record Concatenation and Multiple Inheritance
Regular Grammars for Sets of Graphs of Tree-Width 2
A Modal Mu-Calculus for Durational Transition Systems
Parametric Limits
The Identity Problem in the special affine group of Z 2
An Until Hierarchy for Temporal Logic
An Algebra for Kripke Polynomial Coalgebras
Revisiting reachability in timed automata
Compositional Analysis for Concurrent Constraint Programming
Ordinal Exponentiation in Homotopy Type Theory
On the computational content of Zorn's lemma
Querying the Guarded Fragment
Dinatural Terms in System F
Re-pairing brackets
Undecidable Optimization Problems for Database Logic Programs
Types Are Internal ∞-Groupoids
Games on Graphs and Sequentially Realizable Functionals
Long-run Satisfaction of Path Properties
LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020
Lambda Y-Calculus With Priorities
Elementary Axioms for Categories of Classes
Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
Lambda Calculus and Probabilistic Computation
Invisible Pushdown Languages
Higher Groups in Homotopy Type Theory
Decidability of Linear Affine Logic
Can LCF Be Topped? Flat Lattice models of Typed Lambda Calculus (Preliminary Report)
Register automata with linear arithmetic