yusuke1997/dblp-id-title huggingface dataset:
An Algebraic Theory of Markov Processes
Demonic Lattices and Semilattices in Relational Semigroups with Ordinary Composition
A Decidable Two-Way Logic on Data Words
Logical Hierarchies in PTIME
The Semantics of Parsing with Semantic Actions
Secure Implementation of Channel Abstractions
Continuation Models are Universal for Lambda-Mu-Calculus
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016
Automatic Decidability
Regular Transformations of Infinite Strings
Full Abstraction for First-Order Objects with Recursive Types and Subtyping
Closure Properties of Coalgebra Automata
True Relative Completeness of an Axiom System for the Language L4 (Abridged)
Graphical Affine Algebra
The Sensible Graph Theories of Lambda Calculus
On the Parallel Complexity of Model Checking in the Modal Mu-Calculus
Probabilistic Polynominal-Time Process Calculus and Security Protocol Analysis
Ptime Canonization for Two Variables with Counting
Light Affine Logic
Deterministic Generators and Games for LTL Fragments
From Quantifier Depth to Quantifier Number: Separating Structures with k Variables
The Existence of Finite Abstractions for Branching Time Model Checking
Symmetries of Graphs and Structures that Fail to Interpret a Finite Thing
A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics
Identity Testing for Radical Expressions
Robin Milner, a Craftsman of Tools for the Mind
Functorial Parametricity
Beyond Image-Finiteness: Labelled Transition Systems as a Stone Space
Expressivity of Quantitative Modal Logics : Categorical Foundations via Codensity and Approximation
Highly Acyclic Groups, Hypergraph Covers and the Guarded Fragment
Behavioural Preorders via Graded Monads
Polarity and the Logic of Delimited Continuations
The Ordinal Recursive Complexity of Lossy Channel Systems
An NP Decision Procedure for Protocol Insecurity with XOR
Relational Parametricity and Control
The Geometry of Computation-Graph Abstraction
The Integers as a Higher Inductive Type
A Computational Interpretation of Parametricity
The Complexity of Verbal Languages over Groups
A Logical Characterization of Individual-Based Models
Model-Checking Parse Trees
Origins and Metamorphoses of the Trinity: Logic, Nets, Automata
Finite-valued Streaming String Transducers
Looping Caterpillars
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018
A comonadic view of simulation and quantum resources
Specification and Refinement of Probabilistic Processes
A Functional Quantum Programming Language
A Second-Order System for Polytime Reasoning Using Graedel's Theorem
How to Specify and Verify the Long-Run Average Behavior of Probabilistic Systems
Full Abstraction and Expressive Completenes for FP
Probabilistic Verification by Tableaux
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing
A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
A General Notion of Realizability
Decidable and Undecidable Fragments of First-Order Branching Temporal Logics
Concurrent Separation Logic Meets Template Games
Dense Real-Time Games
Bisimulation and open maps
A Constraint Sequent Calculus
The Hidden Subgroup Problem for Universal Algebras
Partial Objects in the Calculus of Constructions
Quantitative and Qualitative Semantics (Abstract of Invited Lecture)
Unrestricted stone duality for Markov processes
Categories, Allegories and Circuit Design
On the Complexity of Linear Arithmetic with Divisibility
Decomposing Quantified Conjunctive (or Disjunctive) Formulas
Learning Concepts Definable in First-Order Logic with Counting
Constructions with Non-Recursive Higher Inductive Types
Domain Theory and Differential Calculus (Functions of one Variable)
Comonadic semantics for guarded fragments
Descriptive complexity for minimal time of cellular automata
Semantics for two-dimensional type theory
An n! Lower Bound on Formula Size
A Quantum Interpretation of Bunched Logic & Quantum Separation Logic
Typed Normal Form Bisimulation for Parametric Polymorphism
Recursive Polymorphic Types and Parametricity in an Operational Framework
Convergence Results for Relational Bayesian Networks
Removing Redundant Refusals: Minimal Complete Test Suites for Failure Trace Semantics
Model-Checking Hierarchical Structures
Turning SOS Rules into Equations
Definitions by Rewriting in the Calculus of Constructions
A Per Model of Polymorphism and Recursive Types
Plays as Resource Terms via Non-idempotent Intersection Types
Defaults and Revision in Structured Theories
Finite Open-World Query Answering with Number Restrictions
Specification in Software Development
Eager Normal Form Bisimulation
Semantical Paradigms: Notes for an Invited Lecture, with Two Appendices by Stavros S. Cosmadakis
How Good Is a Strategy in a Game with Nature?
Short Propositional Refutations for Dense Random 3CNF Formulas
Verifying higher-order concurrency with data automata
Subtyping and Parametricity
A Multiple-Conclusion Meta-Logic
Forcing MSO on Infinite Words in Weak MSO
Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
When Locality Meets Preservation
Descriptive complexity of linear equation systems and applications to propositional proof complexity
Towards Deductive Synthesis of Dataflow Networks
Better Abstractions for Timed Automata
The Pebble-Relation Comonad in Finite Model Theory
Lower Bounds for the Complexity of Monadic Second-Order Logic
More About Recursive Structures: Descriptive Complexity and Zero-One Laws
Decidability of Definability
Control in o-minimal Hybrid Systems
From positive and intuitionistic bounded arithmetic to monotone proof complexity
Once and For All
Model-checking Trace Event Structures
Universal Semantics for the Stochastic λ-Calculus
Intuitionistic S4 is decidable
Categorical Combinatorics for Innocent Strategies
Linear Types and Non-Size-Increasing Polynomial Time Computation
From Automatic Structures to Borel Structures
A Unifying Approach to the Gamma Question
Decision Problems in Ordered Rewriting
Higher-Order Narrowing
Quantum Expectation Transformers for Cost Analysis
Semantics of Higher-Order Quantum Computation via Geometry of Interaction
A Finiteness Structure on Resource Terms
Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada
A Graph of a Relational Structure and Constraint Satisfaction Problems
Blockchains and the Logic of Accountability: Keynote Address
Fully abstract encodings of λ-calculus in HOcore through abstract machines
Cartesian Closed Double Categories, Their Lambda-Notation, and the Pi-Calculus
20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings
Types and Programming Languages: The Next Generation
A Constructive Formalization of the Catch and Throw Mechanism
A Constructive Logic with Classical Proofs and Refutations
Linear Logic Without Boxes
Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract
The Complexity of Subtype Entailment for Simple Types
0-1 Laws and Decision Problems for Fragments of Second-Order Logic
Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
Towards a Mathematical Operational Semantics
Weighted model counting beyond two-variable logic
Higher Dimensional Multigraphs
On the Limits of Efficient Temporal Decidability (Extended Abstract)
Polynomial Invariants for Affine Programs
Multiplicity Problems on Algebraic Series and Context-Free Grammars
Generalized Majority-Minority Operations are Tractable
Intuitionistic Linear Logic and Partial Correctness
Abstract Saturation-Based Inference
Generalized Quantifiers for Simple Properties
Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity
A New Perspective on FO Model Checking of Dense Graph Classes
Psi-calculi: Mobile Processes, Nominal Data, and Logic
The Isomorphism Problem on Classes of Automatic Structures
Coalgebras, Chu Spaces, and Representations of Physical Systems
The Strength of Replacement in Weak Arithmetic
Unsatisfiable Random Formulas Are Hard to Certify
Stack semantics of type theory
Set-Theoretic and Type-Theoretic Ordinals Coincide
On Subsumption and Semiunification in Feature Algebras
Decomposability, Decidability and Axiomatisability for Bisimulation Equivalence on Basic Parallel Processes
Inverse and Implicit Functions in Domain Theory
Finitary Fairness
An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it
RI: A Logic for Reasoning with Inconsistency
Lacon- and Shrub-Decompositions: A New Characterization of First-Order Transductions of Bounded Expansion Classes
A Relational Theory of Monadic Rewriting Systems, Part I
A Sequent Calculus for Opetopes
Regular Transducer Expressions for Regular Transformations
Relevant S is Undecidable
Light Affine Calculus and Polytime Strong Normalization
Reasoning about Hierarchical Storage
Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes
Term Rewriting and Lambda Calculus
A Tetrachotomy for Positive First-Order Logic without Equality
Session Logical Relations for Noninterference
Logics for continuous reachability in Petri nets and vector addition systems with states
A New Efficient Simulation Equivalence Algorithm
On Proofs about Threshold Circuits and Counting Hierarchies
Semistructured Data: from Practice to Theory
Names and Symmetry in Computer Science (Invited Tutorial)
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory
Proof of Translation in Natural Semantics
Spectra of Monadic Second-Order Formulas with One Unary Function
Large Finite Structures with Few L k -Types
Types for Hereditary Permutators
Quantitative semantics of the lambda calculus: Some generalisations of the relational model
Monadic Queries over Tree-Structured Data
Partial Model Checking (Extended Abstract)
The Space of Interaction
Polynomial-time Algorithms from Ineffective Proofs
Normalization for Cubical Type Theory
Temporal Logic Query Checking
Program Correctness on Finite Fields
Semantic Subtyping for the p-Calculus
Game Semantics for Good General References
Multi-Clock Timed Networks
Deterministic Sub-exponential Algorithm for Discounted-sum Games with Unary Weights
Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata
Equivalence and Conditional Independence in Atomic Sheaf Logic
Database Query Languages Embedded in the Typed Lambda Calculus
A characterisation of ordered abstract probabilities
Automatic Verification of Finite-State Concurrent Systems
Binary symmetries of tractable non-rigid structures
Bialgebraic Reasoning on Higher-order Program Equivalence
34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019
The Omega Rule is II_2^0-Hard in the lambda beta -Calculus
Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom
Around Classical and Intuitionistic Linear Logics
Magnitude Monadic Logic over Words and the Use of Relative Internal Set Theory
Demystifying Reachability in Vector Addition Systems
Realizability in the Unitary Sphere
Hybrid realizability for intuitionistic and classical choice
Fixed Points In Quantitative Semantics
Counting Bounded Tree Depth Homomorphisms
Completeness for typed lazy inequalities
The Computational Behaviour of Girard's Paradox
Simultaneous E-Unification and Related Algorithmic Problems
Monadic second order logic as the model companion of temporal logic
The Category of Constraint Systems is Cartesian-Closed
Complexity of Power Default Reasoning
Model-Checking for Real-Time Systems
A Hennessy-Milner Theorem for ATL with Imperfect Information
Alternating Timed Automata over Bounded Time
Generalizing Parametricity Using Information-flow
Alternating Nominal Automata with Name Allocation
Regular Expressions in Process Algebra
First-order tree-to-tree functions
A modal μ perspective on solving parity games in quasi-polynomial time
Probabilistic Verification Beyond Context-Freeness
Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence
Languages of Dot-Depth One over Infinite Words
Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete
A system of inference based on proof search: an extended abstract
A Tutorial on Finite Model Theory (Abstract)
Order-Incompleteness and Finite Lambda Models (Extended Abstract)
Some Computational Properties of Intersection Types
Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types
Defining Winning Strategies in Fixed-Point Logic
Light Logics and Optimal Reduction: Completeness and Complexity
From Categorical Logic to Facebook Engineering
Stochastic Best-Effort Strategies for Borel Goals
Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithm
The 0-1 law fails for frame satisfiability of propositional modal logic
A Linear Logical Framework
Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs
The Complexity of Global Cardinality Constraints
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
Minimalism subsumes Default Logic and Circumscription in Stratified Logic Programming
Graphs of unbounded linear cliquewidth must transduce all trees
ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network
Parallelism and Synchronization in an Infinitary Context
Temporal Constraint Satisfaction Problems in Fixed-Point Logic
Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
Convergence Law for Random Graphs with Specified Degree Sequence
A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis
Computable PAC Learning of Continuous Features
Formalizing Randomized Matching Algorithms
Simulating Logspace-Recursion with Logarithmic Quantifier Depth
Transition Invariants
A Logical Characterization of Bisimulation for Labeled Markov Processes
High-level methods for homotopy construction in associative n-categories
A Fully Abstract Semantics for a Functional Language with Logic Variables
Combining Nondeterminism, Probability, and Termination: Equational and Metric Reasoning
Parikh's Theorem in Commutative Kleene Algebra
Automatic Sequences and Zip-Specifications
Approximate Verification of the Symbolic Dynamics of Markov Chains
Full abstraction for nominal general references
On the Complexity of Modular Model Checking
The Parallel Intensionally Fully Abstract Games Model of PCF
Turing's Password: What Internet Cannot Leak
A Logician Looks at Expert Systems: Areas for Mathematical Research (Abstract of Invited Lecture)
A short story of the CSP dichotomy conjecture
Basic Paramodulation and Decidable Theories (Extended Abstract)
Approximate Satisfiability and Equivalence
Semantically Acyclic Conjunctive Queries under Functional Dependencies
Algorithms for some infinite-state MDPs and stochastic games
22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings
Quantum channels as a categorical completion
Extensional PERs
Parity objectives in countable MDPs
16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings
Levels of Knowledge in Distributed Computing
Evidenced Frames: A Unifying Framework Broadening Realizability Models
Hanf normal form for first-order logic with unary counting quantifiers
A General Framework for Relational Parametricity
Completeness of Kozen's Axiomatisation of the Propositional mu-Calculus
Kripke-Style models for typed lambda calculus
Computation and the Periodic Table
Categories of Embeddings
Computability Beyond Church-Turing via Choice Sequences
A Why-on-Earth Tutorial on Finite Model Theory
Highly Efficient Secrecy-Preserving Proofs of Correctness of Computations and Applications
Completions of µ-algebras
Wreath Products of Distributive Forest Algebras
Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete
Conservative Concurrency in Haskell
Codensity Games for Bisimilarity
Automata Learning: An Algebraic Approach
3-Valued Abstraction: More Precision at Less Cost
Phase Semantics and Verification of Concurrent Constraint Programs
On the Decidability of Metric Temporal Logic
Trace Semantics is Fully Abstract
A Sound and Complete Calculus for Finite Stream Circuits
Semantic Subtyping
Imperfect information flow
A simple proof system for lock-free concurrency
Approximating Labeled Markov Processes
Conformance Games for Graded Semantics
Pseudorandom Finite Models
Fully Abstract Denotational Semantics for Flat Concurrent Prolog
Classical realizability as a classifier for nondeterminism
Interpretations in Trees with Countably Many Branches
Weak Alternating Automata Give a Simple Explanation of Why Most Temporal and Dynamic Logics are Decidable in Exponential Time
A Generalised Twinning Property for Minimisation of Cost Register Automata
Process Operations in Extended Dynamic Logics
A Proof of Strong Normalisation using Domain Theory
Constructing Higher Inductive Types as Groupoid Quotients
Some Uses of Maximal Fixed Points (Abstract of Invited Lecture)
Computable decision making on the reals and other spaces: via partiality and nondeterminism
Quantifiers on languages and codensity monads
The Proof Complexity of Linear Algebra
Embedded Finite Models, Stability Theory and the Impact of Order
A Continuum of Theories of Lambda Calculus without Semantics
Effectful applicative bisimilarity: Monads, relators, and Howe's method
Emil Post's Contributions to Computer Science
New Conditions for Taylor Varieties and CSP
Lindstrom theorems for fragments of first-order logic
Separation and covering for group based concatenation hierarchies
A Universal Characterization of the Closed Euclidean Interval
Induction in Algebra: A First Case Study
Operator Spaces, Linear Logic and the Heisenberg-Schrödinger Duality of Quantum Theory
Pumping by Typing
δ is for Dialectica
Computing Reachability Relations in Timed Automata
Bounded-Memory Strategies in Partial-Information Games
On Locality and Uniform Reduction
Typability in bounded dimension
Gödel logic: From natural deduction to parallel computation
An Improved Lower Bound for the Complementation of Rabin Automata
A Small Universal Model for System Executions
Modal mu-Types for Processes
Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting
Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998
Nominal Games and Full Abstraction for the Nu-Calculus
Data Communicating Processes with Unreliable Channels
On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata
Bisimulation is Not Finitely (First Order) Equationally Axiomatisable
The Declarative Semantics of the Prolog Selection Rule
Decidability of the Confluence of Ground Term Rewriting Systems
History-Dependent Nominal μ-Calculus
Multi-Structural Games and Number of Quantifiers
Subtype Inequalities
A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations (Preliminary Extended Abstract)
Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes
Describing free $\omega$ -categories
Separation Logic in the Presence of Garbage Collection
Pattern Matching as Cut Elimination
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
Near Unanimity Constraints Have Bounded Pathwidth Duality
Approximation Schemes for First-Order Definable Optimisation Problems
Instances of Computational Effects: An Algebraic Perspective
Group Order Logic
Environmental Bisimulations for Higher-Order Languages
An Algebraic Approach to the Complexity of Propositional Circumscription
The Engineering Challenge for Logic
Separation for dot-depth two
A Simple and Optimal Complementation Algorithm for Büchi Automata
In and Out of Temporal Logic
The Target Discounted-Sum Problem
Parametricity and Semi-Cubical Types
Compiler Verification in LF
Reasonable Space for the λ-Calculus, Logarithmically
Every λ-Term is Meaningful for the Infinitary Relational Model
MDPs with energy-parity objectives
A Higher Structure Identity Principle
The Probabilistic Rabin Tree Theorem *
On the Automata Size for Presburger Arithmetic
From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata
Foundational nonuniform (Co)datatypes for higher-order logic
Region Analysis and the Polymorphic Lambda Calculus
Logic, Complexity, and Games
Logical relations for call-by-push-value models, via internal fibrations in a 2-category
Normalization and Extensionality (Extended Abstract)
Hereditary Harrop Formulas and Uniform Proof Systems
Concrete categories and higher-order recursion: With applications including probability, differentiability, and full abstraction
Recent Developments in Quantitative Information Flow (Invited Tutorial)
Hyper Natural Deduction
Hardware Verification, Boolean Logic Programming, Boolean Functional Programming
A Complete Axiomatization of MSO on Infinite Trees
A Temporal-Logic Approach to Binding-Time Analysis
Cellular Cohomology in Homotopy Type Theory
Horn Programming in Linear Logic Is NP-Complete
Logic Programs as Types for Logic Programs
Completing Gordon's Higher-Order Logic
A type-theoretical definition of weak ω-categories
Two-Variable Logic with Counting is Decidable
New Directions in Instantiation-Based Theorem Proving
Differential Refinement Logic
Weak Bisimulation and Open Maps
An Analysis of Girard's Paradox
McColm's Conjecture
Characterising Choiceless Polynomial Time with First-Order Interpretations
Regular and First-Order List Functions
Duality in Computer Science
Dynamic Logic of Propositional Assignments: A Well-Behaved Variant of PDL
Reactive Systems over Cospans
A General Semantics for Evaluation Logic
Orbit-finite linear programming
Solving Inequations in Term Algebras (Extended Abstract)
The Existence of Refinement Mappings
Quasi-Open Bisimilarity with Mismatch is Intuitionistic
Complexity of Modular Circuits
Inductive Reasoning with Incomplete Specifications (Preliminary Report)
Perspective Multi-Player Games
On the number of types in sparse graphs
Characterizing Positionality in Games of Infinite Duration over Infinite Graphs
Reducts of finitely bounded homogeneous structures, and lifting tractability from finite-domain constraint satisfaction
Domains and Logics (Extended Abstract)
Domains of Commutative C-Subalgebras
On Model-Checking Trees Generated by Higher-Order Recursion Schemes
An Analysis of Symmetry in Quantitative Semantics
Parametric Quantitative Temporal Reasoning
The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems
Descriptive Set Theory in the Category of Represented Spaces
Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
Element-free probability distributions and random partitions
A Neutral Approach to Proof and Refutation in MALL
Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems
A Syntactic Characterization of NP-Completeness
Modular Temporal Logic
Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order Logic
The Geometry of Bayesian Programming
Syntactic Theories and Unification
A categorical approach to open and interconnected dynamical systems
Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics
Adequacy for untyped translations of typed lambda-calculi
What's in a game?: A theory of game models
Computational expressivity of (circular) proofs with fixed points
Categorical liveness checking by corecursive algebras
The Logic of Prefixes and Suffixes is Elementary under Homogeneity *
Querying Visible and Invisible Information
Single-Threaded Polymorphic Lambda Calculus
Full Abstraction for Functional Languages with Control
Stable graphs of bounded twin-width
Floyd-Hoare Logic Defines Semantics: Preliminary Version