yusuke1997/dblp-id-title huggingface dataset:
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA
On the Relationship Between Process Algebra and Input/Output Automata
Tree Extension Algebras: Logics, Automata, and Query Languages
Syntax and Semantics for Operations with Scopes
Turing Machines with Atoms
Axiomatizing Operational Equivalence in the Presence of Side Effects
General Structural Operational Semantics through Categorical Logic
The Complexity of Verifying Ground Tree Rewrite Systems
There is No Recursive Axiomatization for Feasible Functionals of Type~2
Negation As Refutation
The Two-Variable Guarded Fragment with Transitive Relations
Proof-Theoretic Approach to Description-Logic
1-in-3 vs. Not-All-Equal: Dichotomy of a broken promise
Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time
From Thin Concurrent Games to Generalized Species of Structures
The continuity of monadic stream functions
The Largest First-Order-Axiomatizable Cartesian Closed Category of Domains
On the Satisfiability of Context-free String Constraints with Subword-Ordering
Believe it or not, AJM's Games Model is a Model of Classical Linear Logic
Healthiness from Duality
Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or
On sequentiality and well-bracketing in the π-calculus
How Uncomputable is General Circumscription? (Extended Abstract)
The complexity of soundness in workflow nets
Descriptive complexity of real computation and probabilistic independence logic
Efficient On-the-Fly Model Checking for CTL*
Automated Verification of Selected Equivalences for Security Protocols
Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete: Crystallization: Near-Collapsing Process Graph Interpretations of Regular Expressions
The concurrent game semantics of Probabilistic PCF
Diagrammatic Algebra of First Order Logic
Fibred Data Types
An Asynchronous Soundness Theorem for Concurrent Separation Logic
The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain Equations
Rabin Measures and Their Applications to Fairness and Automata Theory
Games with bound guess actions
Automatic Structures: Richness and Limitations
On The Relational Width of First-Order Expansions of Finitely Bounded Homogeneous Binary Cores with Bounded Strict Width
Model Checking Synchronized Products of Infinite Transition Systems
Characterising Testing Preorders for Finite Probabilistic Processes
On the Structure of Queries in Constraint Query Languages
Stochastic Processes with Expected Stopping Time
Logic for Explainable AI
Symbolic Model Checking: 10^20 States and Beyond
Linear Logic, Totality and Full Completeness
Some Methods of Problem Solving in Elementary Geometry
Some constructive variants of S4 with the finite model property
Probabilistic Information Flow
Algebraic models of simple type theories: A polynomial approach
Conditional Lambda-Theories and the Verification of Static Properties of Programs
Recursion Schemes and Logical Reflection
Faster Solutions of Rabin and Streett Games
Local consistency as a reduction between constraint satisfaction problems
Description Logics: Foundations for Class-based Knowledge Representation
On First Order Database Query Languages
Interacting Frobenius Algebras are Hopf
Corrigendum: Complete Type Inference for Simple Objects
Game Semantics in String Diagrams
Two complete axiomatisations of pure-state qubit quantum computing
Reflexive Scott Domains are Not Complete for the Extensional Lambda Calculus
Tarskian Set Constraints
A Bunched Logic for Conditional Independence
Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests
On Model Checking for Non-Deterministic Infinite-State Systems
3rd International Workshop on Logics, Agents, and Mobility, LAM'10, Edinburgh, UK, July 14, 2010
Probabilistic Relational Reasoning via Metrics
Quantum advantage and CSP complexity
The pebbling comonad in Finite Model Theory
Semantic Minimization of 3-Valued Propositional Formulae
Uniformisation of Regular Relations in First-Order Logic with Two Variables
Hofmann-Streicher lifting of fibred categories : Dedicated to the memory of Thomas Streicher (1958-2025)
A Modest Model of Records, Inheritance and Bounded Quantification
Contextual Equivalence for State and Control via Nested Data
Unique Fixpoint Induction for Value-Passing Processes (Extended Abstract)
Trichotomy in the Complexity of Minimal Inference
21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings
The convex hull of finitely generable subsets and its predicate transformer
The Iteration Number of the Weisfeiler-Leman Algorithm
Proof Theory for Kleene Algebra
Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
The Expressive Power of Finitely Many Generalized Quantifiers
Complexity Bounds for Sum-Product Logic via Additive Proof Nets and Petri Nets
Two-way unary temporal logic over trees
Fixed-Points for Quantitative Equational Logics
A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity
Orienting Equalities with the Knuth-Bendix Order
Infinitary Completeness in Ludics
Constructing Fully Complete Models for Multiplicative Linear Logic
Two-Way Visibly Pushdown Automata and Transducers
Pebble Minimization of Polyregular Functions
Complete Cuboidal Sets in Axiomatic Domain Theory
Abstract Machines for Game Semantics, Revisited
A Dichotomy in the Complexity of Propositional Circumscription
Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances
Some Complexity Bounds for Dynamic Logics
Relating Levels of the Mu-Calculus Hierarchy and Levels of the Monadic Hierarchy
Zero-one laws for provability logic: Axiomatizing validity in almost all models and almost all frames
Relational Properties of Recursively Defined Domains
Fixed Point Logics on Hemimetric Spaces
Expressiveness and Closure Properties for Quantitative Languages
Unification in Free Extensions of Boolean Rings and Abelian Groups
Origins of the Calculus of Binary Relations
Interpolation for the two-way modal μ-calculus
A Fragment Calculus - Towards a Model of Separate Compilation, Linking and Binary Compatibility
Mean-Payoff Pushdown Games
Polymorphism, Set Theory, and Call-by-Value
A computable approach to measure and integration theory
A Perfect Model for Bounded Verification
Computational Foundations of Basic Recursive Function Theory
Regularity Preserving but Not Reflecting Encodings
Algebraic and algorithmic synergies between promise and infinite-domain CSPs
Metric Reasoning about λ-Terms: The Affine Case
A van Benthem Theorem for Fuzzy Modal Logic
Ramified Higher-Order Unification
Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete
Logic and regular cost functions
Complexity Theory of (Functions on) Compact Metric Spaces
The Unifiability Problem in Ground AC Theories
Some Desirable Conditions for Feasible Functionals of Type~2
Relators and Notions of Simulation Revisited
Formalized Metareasoning in Type Theory
Second-Order and Dependently-Sorted Abstract Syntax
On the axiomatizability of quantitative algebras
Slice closures of indexed languages and word equations with counting constraints
Playing with Repetitions in Data Words Using Energy Games
Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA
Polarised Intermediate Representation of Lambda Calculus with Sums
Constructive completeness for the linear-time μ-calculus
A Constructive Proof of Dependent Choice, Compatible with Classical Logic
Axiomatizing Net Computations and Processes
Nets and Data Flow Interpreters
Computing with Recursive Types (Extended Abstract)
Induction and Recursion on the Partial Real Line via Biquotients of Bifree Algebras
Quantitative Monadic Second-Order Logic
Strategy logic with imperfect information
Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997
Complexity of Two-Variable Dependence Logic and IF-Logic
Understanding the complexity of #SAT using knowledge compilation
A Semantically Based Proof System for Partial Correctness and Deadlock in CSP
The Computational Meaning of Probabilistic Coherence Spaces
Verifying Infinite Markov Chains with a Finite Attractor or the Global Coarseness Property
Riesz Modal logic for Markov processes
Weak consistency notions for all the CSPs of bounded width
A Propositional Model Logic of Time Intervals
Treelike Decompositions for Transductions of Sparse Graphs
Functional Reachability
A Near-Minimal Axiomatisation of ZX-Calculus for Pure Qubit Quantum Mechanics
A calculus of expandable stores: Continuation-and-environment-passing style translations
A weakest pre-expectation semantics for mixed-sign expectations
Deterministic stream-sampling for probabilistic programming: semantics and verification
Matching μ-Logic
In search of lost time: Axiomatising parallel composition in process algebras
On Program Equivalence in Languages with Ground-Type References
Equicardinality on Linear Orders
Priorities in Process Algebras
Recognizing omega-regular Languages with Probabilistic Automata
An effectful way to eliminate addiction to dependence
Generalised species of rigid resource terms
Automata on Infinite Trees with Equality and Disequality Constraints Between Siblings
32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017
A categorical account of composition methods in logic
Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract)
Pointer Programs and Undirected Reachability
Adapting Logics
Expressive Completeness of Two-Variable First-Order Logic with Counting for First-Order Logic Queries on Rooted Unranked Trees
Semi-galois Categories I: The Classical Eilenberg Variety Theory
Linear vs. Branching Time: A Complexity-Theoretic Perspective
Invertibility in lambda-eta
No-Rainbow Problem and the Surjective Constraint Satisfaction Problem
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events
Nondeterminism in Game Semantics via Sheaves
Proof Nets for Unit-free Multiplicative-Additive Linear Logic (Extended abstract)
Graph Logics with Rational Relations and the Generalized Intersection Problem
Smooth approximations and CSPs over finitely bounded homogeneous structures
Principles of Superdeduction
Strong Sums in Focused Logic
Some Semantic Aspects of Polymorphic Lambda Calculus
Thin Coalgebraic Behaviours Are Inductive
The Curry-Howard Correspondence in Set Theory
Configuration Structures
Quantitative Analysis and Model Checking
Space-efficient Query Evaluation over Probabilistic Event Streams
On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap
Complete Quantum Relational Hoare Logics from Optimal Transport Duality
Quantitative Automata under Probabilistic Semantics
Monadic Theory of Term Rewritings
Model Checking Probabilistic Pushdown Automata
First order complexity of finite random structures
Symbolic Model Checking for Real-time Systems
Decidability of Weak Simulation on One-Counter Nets
Tractability and learnability arising from algebras with few subpowers
Observable Algorithms on Concrete Data Structures
Definability equals recognizability for graphs of bounded treewidth
Foundation for a series of efficient simulation algorithms
Completing Partial Combinatory Algebras With Unique Head-Normal Forms
Multiple Reachability in Linear Dynamical Systems
Hypergraph Acyclicity and Extension Preservation Theorems
The "Hardest" Natural Decidable Theory
Games Semantics for Linear Logic
Linear Dependent Types and Relative Completeness
The Expressive Power of Synchronizations
ALOGTIME and a Conjecture of S. A. Cook (Extended Abstract)
Regular separability of one counter automata
A Bound on Attacks on Payment Protocols
First-Order Reasoning and Efficient Semi-Algebraic Proofs
Transducers of polynomial growth
An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles
Initial Algebra Correspondence under Reachability Conditions
Complexity Lower Bounds from Algorithm Design
If At First You Don't Succeed: Extended Monitorability through Multiple Executions
Zero-One Laws for Modal Logic
The First-Order Theory of Ordering Constraints over Feature Trees
Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses
Completeness of Type Assignment Systems with Intersection, Union, and Type Quantifiers
Polarized Games
Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract)
Proof Search in First-Order Linear Logic and Other Cut-Free Sequent Calculi
Solving Linear Equations over Polynomial Semirings
On shift-invariant maximal filters and hormonal cellular automata
The Logical Role of the Four-Valued Bilattice
On the Verification of Broadcast Protocols
Normal Process Representatives
A Complete Axiomatization of Interval Temporal Logic with Infinite Time
A Fibrational Account of Local States
Implicit Definability on Finite Structures and Unambiguous Computations (Preliminary Report)
Local Action and Abstract Separation Logic
Common knowledge and multi-scale locality analysis in Cayley structures
Higher-Order Model Checking: An Overview
Structural Subtyping of Non-Recursive Types is Decidable
#P is Sandwiched by One and Two #2DNF Calls: Is Subtraction Stronger Than We Thought?
The Structure of First-Order Causality
Partial Order Models of Concurrency and the Computation of Functions
The Satisfiability Problem for Probabilistic CTL
A constructive function-theoretic approach to topological compactness
Rules of Definitional Reflection
The Lazy Lambda Calculus in a Concurrency Scenario (Extended Abstract)
On the Complexity of Reasoning in Kleene Algebra
Possession as Linear Knowledge
The Semantics of Reflected Proof
The Geometry of Interaction of Differential Interaction Nets
Automaton-Based Criteria for Membership in CTL
Full Abstraction and Universality via Realisability
On the Weisfeiler-Leman Dimension of Finite Groups
On the Complexity of Linear Authorization Logics
Successor-Invariant First-Order Logic on Classes of Bounded Degree
Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988
First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees
View-Based Query Processing and Constraint Satisfaction
Separating LREC from LFP
PDL on Steroids: on Expressive Extensions of PDL with Intersection and Converse
Causal Computational Complexity of Distributed Processes
Functionals Using Bounded Information and the Dynamics of Algorithms
Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
Monadic Logic and Automata: Recent Developments
Symbolic Time and Space Tradeoffs for Probabilistic Verification
Definable decompositions for graphs of bounded linear cliquewidth
Active learning for sound negotiations✱
Revisiting Membership Problems in Subclasses of Rational Relations
A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
Verification of randomized security protocols
New Foundations for Fixpoint Computations
Quantum Hoare Logic with Ghost Variables
Modal Logics with Composition on Finite Forests: Expressivity and Complexity
A Sufficient Condition for the Termination of the Direct Sum of Term Rewriting Systems
The Power of Reflective Relational Machines
Type Theory and Recursion (Extended Abstract)
The Groupoid Model Refutes Uniqueness of Identity Proofs
A Categorical Treatment of Ornaments
Deconstructing Shostak
Symmetric Datalog and Constraint Satisfaction Problems in Logspace
Fixpoint operators for 2-categorical structures
Learning Probabilistic Systems from Tree Samples
Fixed-Point Logics on Planar Graphs
Terms, Proofs, and Refinement (Extended abstract)
Calibrating Computational Feasibility by Abstraction Rank
The Diagonal Problem for Higher-Order Recursion Schemes is Decidable
A Syntax for Strictly Associative and Unital ∞-Categories
Discrimination by Parallel Observers
Constructing Free Boolean Categories
The Cost of Punctuality
Quantitative Algebraic Reasoning
On the Unification Problem for Cartesian Closed Categories
Advice about logical AI
Maximum Matching and Linear Programming in Fixed-Point Logic with Counting
Capturing polynomial time using Modular Decomposition
Abstraction in Data Integration
Set Constraints are the Monadic Class
SD-Regular Transducer Expressions for Aperiodic Transformations
Sequential Relational Decomposition
Inductive Types in Homotopy Type Theory
A Generalized Modality for Recursion
Temporal Logics over Unranked Trees
Privacy and the Price of Data
LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic
Isomorphisms of Types in the Presence of Higher-Order References
Cut-free completeness for modal mu-calculus
Behavioural Conformances based on Lax Couplings
Bisimulation for Labelled Markov Processes
Towards a Simply Typed CALculus for Semantic Knowledge Bases
On the Skolem Problem and the Skolem Conjecture
Church Meets Cook and Levin
Descriptive Complexity for counting complexity classes
Fixpoint Logic vs. Infinitary Logic in Finite-Model Theory
Substructure Temporal Logic
Logic Beyond Formulas: A Proof System on Graphs
Herbrand property, finite quasi-Herbrand models, and a Chandra-Merlin theorem for quantified conjunctive queries
Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis
Qualitative Determinacy and Decidability of Stochastic Games with Signals
Normalization by Evaluation for Typed Lambda Calculus with Coproducts
Proof Theory and Semantics of Logic Programs
Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems
Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State
Relational Parametricity for Computational Effects
On the 0-1 Law for the class of Existential Second Order Minimal Gödel Sentences with Equality
Homomorphic Tree Embeddings and Their Applications to Recursive Program Optimization
Fixed Points vs. Infinite Generation
Higher-Order Critical Pairs
Semantics of Name and Value Passing
Recursive Types Reduced to Inductive Types
LICS 2017 foreword
One-Path Reachability Logic
ECC, an Extended Calculus of Constructions
On Computability of Logical Approaches to Branching-Time Property Verification of Programs
Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's
A Decision Procedure for a Class of Set Constraints (Extended Abstract)
Bisimilarity of Pushdown Automata is Nonelementary
An Insider's Guide to Logic in Telecommunications Data
Collapsible Pushdown Automata and Recursion Schemes
Reachability Types, Traces and Full Abstraction
Semantics of Exact Real Arithmetic
Automatic Proofs by Induction in Equational Theories Without Constructors
The internal languages of univalent categories
Efficient Analysis of VASS Termination Complexity
30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015
A Theory of Register Monitors
The amazing mixed polynomial closure and its applications to two-variable first-order logic
A First-Order Theory of Types and Polymorphism in Logic Programming
Continuous One-Counter Automata
Approximating Values of Generalized-Reachability Stochastic Games
Lower Bounds for Existential Pebble Games and k-Consistency Tests
Tarski's Influence on Computer Science
Characterization and Decidability of FC-Definable Regular Languages
Backward induction in games of perfect information
A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine
y = 2x vs. y = 3x
Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes
Retracts in simply typed lambda-beta-eta-calculus
A Typed Pattern Calculus
Solvability of orbit-finite systems of linear equations
The HOM Problem is EXPTIME-Complete
Quantitative Reasoning for Proving Lock-Freedom
Intermediate problems in modular circuits satisfiability
18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings
On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems
Completeness for arbitrary finite dimensions of ZXW-calculus, a unifying calculus
Automated Production of Traditional Proofs for Constructive Geometry Theorems
First-order logic with reachability for infinite-state systems
Partial Objects In Constructive Type Theory
Orderings for Equational Proofs
Game Semantics and Subtyping
Dual-context calculi for modal logic
Probability monads with submonads of deterministic states
Applications of Game Semantics: From Program Analysis to Hardware Synthesis
Adding an Equivalence Relation to the Interval Logic ABB: Complexity and Expressiveness
Stochastic mechanics of graph rewriting
Partial-Observation Stochastic Games: How to Win When Belief Fails
The Complexity of Neutrals in Linear Logic
Automata-Driven Automated Induction
Caterpillar Duality for Constraint Satisfaction Problems
Decidability of Quasi-Dense Modal Logics
The algebraic dichotomy conjecture for infinite domain Constraint Satisfaction Problems
A Step Up in Expressiveness of Decidable Fixpoint Logics
Quantified Constraints and Containment Problems
Foundational Proof-Carrying Code
Encoding the Calculus of Constructions in a Higher-Order Logic
Expressive Completeness for Metric Temporal Logic
No Go Theorems: Directed Containers That Do Not Distribute Over Distribution Monads
The real projective spaces in homotopy type theory
Quantified Equality Constraints
Inference Rules for Rewrite-Based First-Order Theorem Proving
Equivalence of inductive definitions and cyclic proofs under arithmetic
An Inverse of the Evaluation Functional for Typed lambda-calculus
Logic in Access Control
Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice
On the Termination Problem for Probabilistic Higher-Order Recursive Programs
Strong Bisimulation of State Automata
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
On Typability for Rank-2 Intersection Types with Polymorphic Recursion
Regular Functions and Cost Register Automata
A Higher-Order Indistinguishability Logic for Cryptographic Reasoning
Order-Invariance of Two-Variable Logic is Decidable
On the Formal Semantics of Statecharts (Extended Abstract)
Entailment of Atomic Set Constraints is PSPACE-Complete
Upper and Lower Bounds for Tree-Like Cutting Planes Proofs
Trace semantics for polymorphic references
Counting and Addition Cannot Express Deterministic Transitive Closure
Systems of Set Constraints with Negative Constraints are NEXPTIME-Complete
Alternation-free modal mu-calculus for data trees
Responsibility and verification: Importance value in temporal logics
Subtyping Recursive Types in Kernel Fun
Program Equivalence is Coinductive
Concurrent Omega-Regular Games
A Fully Abstract Semantics for Concurrent Graph Reduction
Guarded Computational Type Theory
On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity
Axioms for Knowledge and Time in Distributed Systems with Perfect Recall
An Axiomatics for Categories of Transition Systems as Coalgebras
Towards a more efficient approach for the satisfiability of two-variable logic
Smart Choices and the Selection Monad
About Translations of Classical Logic into Polarized Linear Logic
Weak Equivalences in Psi-Calculi
Context Matching for Compressed Terms
How Complete is PER?
Coinductive Proof Principles for Stochastic Processes
Decidability and Complexity of Decision Problems for Affine Continuous VASS
Cut-Restriction: From Cuts to Analytic Cuts
A convenient category for higher-order probability theory
Abstract Hidden Markov Models: A Monadic Account of Quantitative Information Flow
Learning Weighted Automata over Number Rings, Concretely and Categorically
One Context Unification Problems Solvable in Polynomial Time
A Linear Semantics for Allowed Logic Programs
Ultrametric Semantics of Reactive Programs
Timed and Probabilistic I/O Automata
How Much Memory is Needed to Win Infinite Games?
Nonlocal Flow of Control and Kleene Algebra with Tests
Passivity and Independence
A Modal Process Logic