yusuke1997/dblp-id-title huggingface dataset:
Local and asynchronous beta-reduction (an analysis of Girard's execution formula)
A Model-Theoretic Approach to Regular String Relations
The Regular Languages of First-Order Logic with One Alternation
Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory
Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete
Domain Theory in Stochastic Processes
Decidable Elementary Modal Logics
Permutation Rewriting and Algorithmic Verification
Genericity Through Stratification
Perturbed Turing Machines and Hybrid Systems
On the Expressiveness of Linearity vs Persistence in the Asychronous Pi-Calculus
Graph Planning with Expected Finite Horizon
Automata, Tableaus and a Reduction Theorem for Fixpoint Calculi in Arbitrary Complete Lattices
An Automata Model for Trees with Ordered Data Values
Model checking for probability and time: from theory to practice
The Cartesian Closed Bicategory of Thin Spans of Groupoids
The Theory of Traces for Systems with Nondeterminism and Probability
A Sound Framework for Untrusted Verification-Condition Generators
Star Height via Games
Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy
Unification nets: canonical proof net quantifiers
Measurable Spaces and Their Effect Logic
PTAS for Sparse General-Valued CSPs
On the Expression of Monadic Second-Order Graph Properties Without Quantifications Over Sets of Edges (Extended Abstract)
Uniformisations of Regular Relations Over Bi-Infinite Words
On the Satisfiability of Some Simple Probabilistic Logics
What's Decidable about Halpern and Shoham's Interval Logic? The Maximal Fragment ABBL
On computability and tractability for infinite sets
Precongruence Formats for Decorated Trace Preorders
On the Eventuality Operator in Temporal Logic
A fine-grained hierarchy of hard problems in the separated fragment
Extending ALCQIO with Trees
Paramodulation without Duplication
A Fully Abstract Game Semantics for General References
Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT
Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Riesz Modal Logic with Threshold Operators
Perspective Games
On the Completeness of Interpolation Algorithms
Integration in Real PCF
Distal Combinatorial Tools for Graphs of Bounded Twin-Width
Finitely Monotone Properties
Strong Normalization as Safe Interaction
Two-Variable Logic on Words with Data
Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
A Characterisation of First-Order Constraint Satisfaction Problems
A Theory of Testing for Real-Time
Full Abstraction for a Shared Variable Parallel Language
Efficient Inference of Object Types
Solving Disequations
An Approach to Regular Separability in Vector Addition Systems
Statistic Analysis for Probabilistic Processes
Capturing Polynomial Time on Interval Graphs
Folding interpretations
Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives
A Probabilistic and Non-Deterministic Call-by-Push-Value Language
A Dependent Set Theory
Bar induction: The good, the bad, and the ugly
An Algebraic Theory of Process Efficiency
Impredicative Encodings of (Higher) Inductive Types
On Definability of Order in Logic with Choice
On Logics and Homomorphism Closure
Long-Run Average Behaviour of Probabilistic Vector Addition Systems
Taylor Expansion as a Monad in Models of DiLL
Making Concurrency Functional
The Complexity of Boundedness for Guarded Logics
The Crane Beach Conjecture
Boolean Expression Diagrams (Extended Abstract)
A Partially Deadlock-Free Typed Process Calculus
Compositionality via Cut-Elimination: Hennessy-Milner Logic for an Arbitrary GSOS
Locally Excluding a Minor
a modal logic for subjective default reasoning
Braids, Twists, Trace and Duality in Combinatory Algebras
The Complexity of Positive First-order Logic without Equality
A Sequent Calculus for Nominal Logic
On Translating Lambda Terms into Combinators; The Basis Problem
A Kantorovich-Monadic Powerdomain for Information Hiding, with Probability and Nondeterminism
On Finite Satisfiability of Two-Variable First-Order Logic with Equivalence Relations
Rigid E-Unification is NP-Complete
Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Satisfiability in multi-valued circuits
Normalisation is Insensible to lambda-Term Identity or Difference
Logics with Rank Operators
Probabilistic Böhm Trees and Probabilistic Separation
On the Consistency of "Truly Concurrent" Operational and Denotational Semantics (Extended Abstract)
Block products for algebras over countable words and applications to logic
Cones as a model of intuitionistic linear logic
First-order Predicate Logic as a Common Basis for Relational and Functional Programming (Abstract)
Predicative Type Universes and Primitive Recursion
Programs, grammars and arguments: a personal view of some connections between computation, language and logic
Automata with Group Actions
Reconciling Population and Agent Models for Crowd Dynamics
Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation
Syllepsis in Homotopy Type Theory
A functional interpretation with state
New Foundations for the Geometry of Interaction
First-Order Logic with Two Variables and Unary Temporal Logic
On the Equivalence of Weak Second Order and Nonstandard Time Semantics For Various Program Verification Systems
The Complexity of Evaluating First-Order Sentences over a Fixed Structure
A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
Infinite sets that admit fast exhaustive search
Refinement-Based Game Semantics for Certified Abstraction Layers
Reasoning about Recursive Probabilistic Programs
A Fixed Point Theorem on Lexicographic Lattice Structures
An Exponential Separation between the Matching Principle and the Pigeonhole Principle
Black Ninjas in the Dark: Formal Analysis of Population Protocols
Applications of Information Inequalities to Database Theory Problems
Rabin-Mostowski Index Problem: A Step beyond Deterministic Automata
Geometric decision procedures and the VC dimension of linear arithmetic theories
Structural Logical Relations
Static analysis of deterministic negotiations
Allegories of Symbolic Manipulations
The Ordinal-Recursive Complexity of Timed-arc Petri Nets, Data Nets, and Other Enriched Nets
Large and Infinitary Quotient Inductive-Inductive Types
Typechecking XML Views of Relational Databases
Non-Elementary Compression of First-Order Proofs in Deep Inference Using Epsilon-Terms
Logical Definability and Query Languages over Unranked Trees
Group Separation Strikes Back
Cutting Planes and constant depth Frege proofs
On Completeness of the mu-calculus
A Constructive Model of Directed Univalence in Bicubical Sets
On Exact Sampling in the Two-Variable Fragment of First-Order Logic
Higher-Order Matching, Games and Automata
A Second-Order Theory for NL
A fixed point extension of the second order lambda-calculus: observable equivalences and models
Unified Algebras and Institutions
A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping
Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
First-order Queries on Finite Structures over the Reals
On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi
Quantifying Over Trees in Monadic Second-Order Logic
Deciding Definability in FO 2 (<) (or XPath) on Trees
A tier-based typed programming language characterizing Feasible Functionals
Graph Reachability and Pebble Automata over Infinite Alphabets
A Developer-oriented Hoare Logic
Bounding the Weisfeiler-Leman Dimension via a Depth Analysis of I/R-Trees
The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi
Conjunctive Types and Algol-like Languages
Addition-Invariant FO and Regularity
A Landscape with Games in the Backgroun
Reachability in Injective Piecewise Affine Maps
The Boundedness Problem for Monadic Universal First-Order Logic
Sequentiality and Strong Stability
The State Complexity of Alternating Automata
Weak Topology and a Differentiable Operator for Lipschitz Maps
A Complete Axiomatization of Knowledge and Cryptography
Compositional Taylor expansion in cartesian differential categories
Unification and Anti-Unification in the Calculus of Constructions
The Quest for a Logic Capturing PTIME
On the Complexity of Epistemic Reasoning
Inheritance and Explicit Coercion (Preliminary Report)
A Type Theory for Strictly Unital ∞-Categories
Games and Definability for System F
Notational definition-a formal account
First-Order and Temporal Logics for Nested Words
The Logic of Exact Covers: Completeness and Uniform Interpolation
Fusible numbers and Peano Arithmetic
Temporal Specifications with Accumulative Values
Complete Type Inference for Simple Objects
Interaction Laws of Monads and Comonads
Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule
Type Reconstruction in Finite-Rank Fragments of the Polymorphic lambda-Calculus (Extended Summary)
Capsules and Separation
On the logical structure of choice and bar induction principles
Examining The Fragments of G
On the Expressiveness and Decidability of Higher-Order Process Calculi
Weak Similarity in Higher-Order Mathematical Operational Semantics
Vector Addition Tree Automata
From Monadic Second-Order Definable String Transformations to Transducers
Type Inference for Recursive Definitions
Tree-Like Counterexamples in Model Checking
On the Expressive Power of CTL
Complete Game Logic with Sabotage
The Semantic Challenge of Verilog HDL
The commutativity problem for effective varieties of formal series, and applications
On Noetherian Spaces
On the Expressivity of Symmetry in Event Structures
PSPACE Bounds for Rank-1 Modal Logics
Formal Verification at Intel
CCS with Priority Choice
Verifying Unboundedness via Amalgamation
A Fully Abstract Semantics for a Concurrent Functional Language with Monadic Types
A Type Theory for Defining Logics and Proofs
Compositional Model Checking
Non-Deterministic Games and Program Analysis: An Application to Security
Separation Logic: A Logic for Shared Mutable Data Structures
Higher Dimensional Transition Systems
Timed Systems through the Lens of Logic
Substructural Operational Semantics as Ordered Logic Programming
On Thin Air Reads Towards an Event Structures Model of Relaxed Memory
Model-checking for successor-invariant first-order formulas on graph classes of bounded expansion
An Operational Semantics for Network Datalog
On the Forms of Locality over Finite Models
On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups
MSO Queries on Trees: Enumerating Answers under Updates Using Forest Algebras
Foundations of Timed Concurrent Constraint Programming
Assigning Types to Processes
Bisimulation Finiteness of Pushdown Systems Is Elementary
Disjunctive Strictness Analysis
Multidimensional beyond Worst-Case and Almost-Sure Problems for Mean-Payoff Objectives
Continuous Random Variables
Modelling Shared State in a Shared Action Model
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes
On the Complexity of Temporal Equilibrium Logic
The Complexity of Model Checking Multi-stack Systems
A Logic for Locally Complete Abstract Interpretations
More Past Glories
Breaking Paths in Atomic Flows for Classical Logic
Modal and Guarded Characterisation Theorems over Finite Transition Systems
Automatic Structures
Solvability of Matrix-Exponential Equations
Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus
A Cubical Approach to Synthetic Homotopy Theory
Homological Invariants of Higher-Order Equational Theories
On the Magnitude of Completeness Thresholds in Bounded Model Checking
On the Arithmetic Inexpressiveness of Term Rewriting Systems
New Notions of Reduction and Non-Semantic Proofs of beta-Strong Normalization in Typed lambda-Calculi
Categorical models of Linear Logic with fixed points of formulas
Towards a Theory of Bisimulation for Local Names
On the Expressiveness and Complexity of Randomization in Finite State Monitors
Constraint Satisfaction Problems over Finite Structures
Probabilistic Stable Functions on Discrete Cones are Power Series
Canonisation and Definability for Graphs of Bounded Rank Width
Logician in the Land of OS: Abstract State Machines in Microsoft
Timed Pushdown Automata Revisited
Syntactic Effectful Realizability in Higher-Order Logic
Path Logics for Querying Graphs: Combining Expressiveness and Efficiency
Lean and full congruence formats for recursion
A Logical Account for Linear Partial Differential Equations
Uniform Distributed Synthesis
Entailment among Probabilistic Implications
The Hierarchy of Hyperlogics
Transductions of Graph Classes Admitting Product Structure
Ludics Nets, a game Model of Concurrent Interaction
When is "Partial" Adequate? A Logic-Based Proof Technique Using Partial Specifications
Separating DAG-Like and Tree-Like Proof Systems
Decision Problems for Semi-Thue Systems with a Few Rules
Games and Full Abstraction for the Lazy lambda-Calculus
Little Engines of Proof
Decidability of DPDA Language Equivalence via First-Order Grammars
Characterization of typings in polymorphic type discipline
The Complexity of First-Order and Monadic Second-Order Logic Revisited
Functional Stream Semantics for a Synchronous Block-Diagram Compiler
Limits of Multi-Discounted Markov Decision Processes
On the Deduction Rule and the Number of Proof Lines
Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives
Syntactic Considerations on Recursive Types
A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages
On the Strictness of the First-Order Quantifier Structure Hierarchy over Finite Structures
Ordering Finite Variable Types with Generalized Quantifiers
Bisimulation in Name-Passing Calculi without Matching
A Complexity Dichotomy for Semilinear Target Sets in Automata with One Counter
Fixed-Parameter Hierarchies inside PSPACE
Equality In Lazy Computation Systems
The Role of Decidability in First Order Separations over Classes of Finite Structures
Deciding the Value 1 Problem for Probabilistic Leaktight Automata
Non-Determinism in a Functional Setting
Prop revisited: Propositional Formula as Abstract Domain for Groundness Analysis
A Symmetric Modal Lambda Calculus for Distributed Computing
Herbrand Constraint Abduction
Comparing Chemical Reaction Networks: A Categorical and Algorithmic Perspective
The Ultimate Undecidability Result for the Halpern-Shoham Logic
Pushdown Model Checking above the Cubic Bottleneck
Proof Nets and Boolean Circuits
Tree Canonization and Transitive Closure
Temporal Linear Logic Specifications for Concurrent Processes (Extended Abstract)
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), Paris, France, July 4-7, 1994
Sound up-to techniques and Complete abstract domains
Guarded Fixed Point Logic
A sequent calculus with dependent types for classical arithmetic
On the Verification Problem of Nonregular Properties for Nonregular Processes
Abstract Syntax and Variable Binding
Good Rewrite Strategies for FP
Canonical Polymorphisms of Ramsey Structures and the Unique Interpolation Property
Modular Construction of Fixed Point Combinators and Clocked Bohm Trees
Fibred fibration categories
Conflict nets: Efficient locally canonical MALL proof nets
Qualitative Tree Languages
Listings and Logics
A distributed operational view of Reversible Prime Event Structures
Minimal Equational Theories for Quantum Circuits
Linear combinations of unordered data vectors
Functional Unification of Higher-Order Patterns
Efficient and Flexible Matching of Recursive Types
Synthesizing Distributed Systems
An Algebra and a Logic for NC¹
Small Substructures and Decidability Issues for First-Order Logic with Two Variables
The Dichotomy for Conservative Constraint Satisfaction Problems Revisited
From Two-Way to One-Way Finite State Transducers
Towards a Logic for Reasoning About Learning in a Changing World
An Algebraic Preservation Theorem for Aleph-Zero Categorical Quantified Constraint Satisfaction
Monadic Second-Order Logic and Hypergraph Orientation
Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes
Size measures and alphabetic equivalence in the μ-calculus
Linear Termination is Undecidable
Distributed Graph Automata
Name-Passing Calculi: From Fusions to Preorders and Types
Equational Prgoramming in lambda-calculus
A tale of intersection types
Modal Intuitionistic Logics as Dialgebraic Logics
A Compositional Semantics for the Reversible p-Calculus
Modularity of Strong Normalization and Confluence in the algebraic-lambda-Cube
Separating Markov's Principles
Type-two polynomial-time and restricted lookahead
28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013
Modal Location-Resource-Process Logic for Access Control
Resource-Bounded Continuity and Sequentiality for Type-Two Functionals
Some Results on Automatic Structures
The Complexity of Resilience Problems via Valued Constraint Satisfaction Problems
Reactive Modules
Faithful Ideal Models for Recursive Polymorphic Types
A Syntactic Approach to Foundational Proof-Carrying Code
On the Decision Problem for the Guarded Fragment with Transitivity
The Logic of Action Lattices is Undecidable
A lambda calculus of objects and method specialization
Coinductive Techniques for Operational Equivalence of Interaction Nets
Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989
Injective hardness condition for PCSPs
Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism Problem
Enumeration reducibility in closure spaces with applications to logic and algebra
Semantics of Separation-Logic Typing and Higher-Order Frame Rules
When is the partial map classifier a Sierpiński cone?
A Diagrammatic Axiomatisation for Qubit Entanglement
The Classification of Continuous Domains (Extended Abstract)
Multiplicative Rewards in Markovian Models
Completeness of a Relational Calculus for Program Schemes
Full Completeness of the Multiplicative Linear Logic of Chu Spaces
A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations
Regular Cost Functions over Finite Trees
On Computational Open-Endedness in Martin-Löf's Type Theory
Proceedings of the Fifth International Workshop on Implicit Computational Complexity, ICC@LICS 2003, Ottawa, Canada, June 26-27, 2003
Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages
Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution
System ST \beta-reduction and completeness
Separation with Streams in the lambdaµ-calculus
Higher-Order Model Checking: From Theory to Practice
Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs
The clocks are ticking: No more delays!
A Logic of Concrete Time Intervals (Extended Abstract)
HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories
Varieties of Quantitative Algebras and Their Monads
The Complexity of Decomposing Modal and First-Order Theories
Decidability, complexity, and expressiveness of first-order logic over the subword ordering
The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes
Path Spaces of Higher Inductive Types in Homotopy Type Theory
Tree-depth, quantifier elimination, and quantifier rank
Successive Approximation of Abstract Transition Relations
Minimal History-Deterministic Co-Büchi Automata: Congruences and Passive Learning
Timed pushdown automata and branching vector addition systems
Characterizing X-Separability and One-Side Invertibility in lambda-beta-Omega-Calculus
When Reachability Meets Grzegorczyk
Parikh Images of Grammars: Complexity and Applications
Powermonads and Tensors of Unranked Effects
The Higher-Order Recursive Path Ordering
Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes
A Calculus of Contracting Processes
Forbidden Induced Subgraphs and the Łoś-Tarski Theorem
Fixed-Point Definability and Polynomial Time on Graphs with Excluded Minors
A Fully-Abstract Model for the pi-Calculus (Extended Abstract)
Combining Generic Judgments with Recursive Definitions
Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF
Branching Bisimilarity of Normed BPA Processes Is in NEXPTIME
Memoryful Branching-Time Logic
Random Variables, Conditional Independence and Categories of Abstract Sample Spaces
Boundedness vs. Unboundedness of Lock Chains: Characterizing Decidability of Pairwise CFL-Reachability for Threads Communicating via Locks
Complexity of LTL Model-Checking for Safe Object Nets
Observational Equivalence of 3rd-Order Idealized Algol is Decidable
Non-Well-Founded Sets Obtained from Ideal Fixed Points
A Canonical Form for Weighted Automata and Applications to Approximate Minimization
Locally Finite Constraint Satisfaction Problems
Extensions of ω-Regular Languages
Games and Full Abstraction for FPC
Factor Varieties and Symbolic Computation
A Relational Account of Call-by-Value Sequentiality
The Definitional Side of the Forcing
Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
Existential Positive Types and Preservation under Homomorphisisms
Imperative Programs as Proofs via Game Semantics
On the Existence of Effective Hoare Logics
Reflexive Graphs and Parametric Polymorphism
Divide and Congruence II: Delay and Weak Bisimilarity
The Complexity of Resolution Refinements
A Logic for Reasoning with Higher-Order Abstract Syntax
Language Completeness of the Lambek Calculus
The Logic of Graph Neural Networks
Domains and event structures for fusions
Atomic Lambda Calculus: A Typed Lambda-Calculus with Explicit Sharing
Differentiable Causal Computations via Delayed Trace
A Trace Based Extension of Linear Time Temporal Logic
Combining Deduction Modulo and Logics of Fixed-Point Definitions
Better is Better than Well: On Efficient Verification of Infinite-State Systems
The Undecidability of System F Typability and Type Checking for Reductionists
Unified Semantics and Proof System for Classical, Intuitionistic and Affine Logics
Universal Domains in the Theory of Denotational Semantics of Programming Languages
Complexity of Normal Default Logic and Related Modes of Nonmonotonic Reasoning
Asynchronous Template Games and the Gray Tensor Product of 2-Categories
Declassification Policy for Program Complexity Analysis
Hoare Logic for Lambda-Terms as Basis of Hoare Logic for Imperative Languages
Automata-Based Abstraction Refinement for µHORS Model Checking
Trading Performance for Stability in Markov Decision Processes
Differentiation in logical form
On the Relative Usefulness of Fireballs
The limits of SDP relaxations for general-valued CSPs
Computing the Density of the Positivity Set for Linear Recurrence Sequences
Verifying linear temporal specifications of constant-rate multi-mode systems
Combining Ehrenfeucht-Fraïssé Games
Bounds in w-Regularity
40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025
Forcing as a Program Transformation
Sequential Colimits in Homotopy Type Theory
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Infinite State AMC-Model Checking for Cryptographic Protocols
Satisfiability in Alternating-time Temporal Logic
Finite Model Theory of the Triguarded Fragment and Related Logics
On Tractability and Congruence Distributivity
On Substitutional Recursion Over Non-Well-Founded Sets
Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs
Combining Algebra and Higher-Order Types
Natural numbers from integers
Interaction Graphs: Full Linear Logic
Temporal Team Semantics Revisited
Quotients in monadic programming: Projective algebras are equivalent to coalgebras
Type Theory via Exact Categories
Successor-Invariance in the Finite
Complete Axioms for Categorical Fixed-Point Operators