yusuke1997/dblp-id-title huggingface dataset:
Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability
Fixed-Point Definability and Polynomial Time
Discreet Games, Light Affine Logic and PTIME Computation
Inductive-Inductive Definitions
Generating All Abductive Explanations for Queries on Propositional Horn Theories
Topological Queries in Spatial Databases
Categorical Duality Theory: With Applications to Domains, Convexity, and the Distribution Monad
A Proof of Kamp's theorem
A Third-Order Bounded Arithmetic Theory for PSPACE
Local temporal reasoning
A characterization of the Taylor expansion of lambda-terms
Normalization of IZF with Replacement
Resource Tableaux
Church-Rosser Properties of Normal Rewriting
On the Representation of Data in Lambda-Calculus
Surjectivity for Finite Sets of Combinators by Weak Reduction
An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games
The Ackermann Award 2007
Simulation by Rounds of Letter-To-Letter Transducers
Monotone Fixed-Point Types and Strong Normalization
Second-Order Equational Logic (Extended Abstract)
Resolution Method for Modal Logic with Well-Founded Frames
Learning by Teams from Examples with Errors
Applying Rewriting Techniques to the Verification of Erlang Processes
Directed Virtual Reductions
From Classical Proof Theory to P versus NP: a Guide to Bounded Theories (Invited Talk)
Parallelism in Soft Linear Logic
A Fully Abstract Relational Model of Syntactic Control of Interference
Completeness for Coalgebraic Fixpoint Logic
Glueability of Resource Proof-Structures: Inverting the Taylor Expansion
A Fast Garbage Collection Algorithm for WAM-Based Prolog
Parity of Imperfection of Fixing Independence
Descriptive Complexity, Lower Bounds and Linear Time
Inductive Inference and Epistemic Modal Logic (Invited Talk)
Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory
Strong Normalization of the Typed gamma ws -Calculus
A Finitary Analogue of the Downward Löwenheim-Skolem Property
The Ackermann Award 2016
Model Theory in Computer Science: My Own Recurrent Themes
Computing with Sequences, Weak Topologies and the Axiom of Choice
Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract)
A Deep Quantitative Type System
Order Structures on Böhm-Like Models
From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
Unifying Cubical Models of Univalent Type Theory
Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings
On Functions Computable in Nondeterministic Polynomial Time: Some Characterizations
Invariant Definability and P/ poly
Enriching an Effect Calculus with Linear Types
Weighted Automata and Expressions over Pre-Rational Monoids
Pre-logical Relations
Decidability of Term Algebras Extending Partial Algebras
Improved Decision Procedures for the Modal Logics K, T, and S4
The Complexity of Adaptive Error-Correcting Codes
Inferring Symbolic Automata
Enhanced Induction in Behavioural Relations (Invited Talk)
System T and the Product of Selection Functions
On the (In)Succinctness of Muller Automata
Computer Science Logic, 7th Workshop, CSL '93, Swansea, United Kingdom, September 13-17, 1993, Selected Papers
Higher-Order Matching in the Linear lambda-calculus with Pairing
The Best a Monitor Can Do
On Test Classes for Universal Theories
Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations
Computer Science Logic, 13th International Workshop, CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings
Weak MSO: automata and expressiveness modulo bisimilarity
The Theory of Calculi with Explicit Substitutions Revisited
On a Generalisation of Herbrand's Theorem
ERRATA to "The Semantics of the C Programming Language"
Well-Founded Recursive Relations
Towards an Efficient Tableau Proof Procedure for Multiple-Valued Logics
On the Emptiness Problem of Tree Automata and Completeness of Modal Logics of Programs
On the total variation distance of labelled Markov chains
Algorithmic Proof with Diminishing Resources, Part 1
An Evolving Algebra Abstract Machine
Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic
Symbolic Automata Theory with Applications (Invited Talk)
Algebra for Tree Languages
Parity Games: Another View on Lehtinen's Algorithm
A Hierarchical Approach to Monadic Second-Order Logic over Graphs
On the Completeness of Narrowing as the Operational Semantics of Functional Logic Programming
Applicative Control and Computational Complexity
RPO Constraint Solving Is in NP
Monadic Presentations of Lambda Terms Using Generalized Inductive Types
Induction in the Elementary Theory of Types and Names
Generalized Connectives for Multiplicative Linear Logic
Equi-Rank Homomorphism Preservation Theorem on Finite Structures
A Proof-Theoretical Investigation of Zantema's Problem
Functorial String Diagrams for Reverse-Mode Automatic Differentiation
From determinism, non-determinism and alternation to recursion schemes for P, NP and Pspace (Invited Talk)
A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata
Partial Fixed-Point Logic on Infinite Structures
Specification Refinement with System F
Knowledge Spaces and the Completeness of Learning Strategies
A Fully Abstract Game Semantics for Countable Nondeterminism
Nondeterminism and Observable Sequentiality
Computer Science Logic, 6th Workshop, CSL '92, San Miniato, Italy, September 28 - October 2, 1992, Selected Papers
Extensions and Limits of the Specker-Blatter Theorem
Game-Based Notions of Locality Over Finite Models
Towards a Typed Geometry of Interaction
Decidable Extensions of Church's Problem
On Compositionality of Dinatural Transformations
Banach-Mazur Games with Simple Winning Strategies
On the Average Time Complexity of Set Partitioning
Negation-Complete Logic Programs
Logical Characterizations of PSPACE
Frontmatter, Table of Contents, Preface, Conference Organization
Relativizing Small Complexity Classes and Their Theories
The Worst-Case Complexity of Symmetric Strategy Improvement
Full Abstractness for a Functional/Concurrent Language with Higher-Order Value-Passing (Extended Abstract)
Dependency Concepts up to Equivalence
The Ackermann Award 2008
On Isomorphisms of Intersection Types
Elementary Modal Logics over Transitive Structures
Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games
Synthesizing Optimally Resilient Controllers
Undecidable First-Order Theories of Affine Geometries
Automated Verification = Graphs, Automata, and Logic
Algorithmic Structuring of Cut-free Proofs
Axioms and decidability for type isomorphism in the presence of sums
Monadic Second Order Finite Satisfiability and Unbounded Tree-Width
Least and Greatest Fixed Points in Ludics
Omega-Branching Programs of Bounded Width
Fully Abstract Models of the Probabilistic lambda-calculus
On Sharply Bounded Length Induction
Constraint Satisfaction with Countable Homogeneous Templates
Logical Omniscience Via Proof Complexity
A Sequent Calculus for Type Theory
Linear Game Automata: Decidable Hierarchy Problems for Stripped-Down Alternating Tree Automata
A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem
Possible World Semantics for General Storage in Call-By-Value
A First Order Theory of Diagram Chasing
Inclusion Logic and Fixed Point Logic
A Tight Karp-Lipton Collapse Result in Bounded Arithmetic
Going Deep and Going Wide: Counting Logic and Homomorphism Indistinguishability over Graphs of Bounded Treedepth and Treewidth
A Game-Theoretic, Concurrent and Fair Model of the Typed Lambda-calculus, with Full Recursion
Description Complexity of Unary Structures in First-Order Logic with Links to Entropy
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
Automata, Logic, and XML
Constrained Hyper Tableaux
The Anatomy of Innocence
The Natural Order-Generic Collapse for omega-Representable Databases over the Rational and the Real Ordered Group
Finite-Memory Strategies in Two-Player Infinite Games
Higher-Order Matching and Tree Automata
Logical Specification of Operational Semantics
The Structural lambda -Calculus
Theorems af Péter and Parsons in Computer Programming
Logical Inference and Polyhedral Projection
Negation as Inconsistency in PROLOG via Intuitionistic Logic
Realising Intensional S4 and GL Modalities
First Order Logic, Fixed Point Logic and Linear Order
Subtyping with Power Types
Strong Induction Is an Up-To Technique
Model Checking of Persistent Petri Nets
The Lambda Calculus Is Quantifiable
Semantic Characterisations of Second-Order Computability over the Real Numbers
A Principle of Induction
Correctness of Multiplicative (and Exponential) Proof Structures is NL -Complete
A Rewriting Theory for Quantum λ-Calculus
Enforcement of Integrity Constraints in a Semantic Data Model
Exponentials with Infinite Multiplicities
On the Role of Type Decorations in the Calculus of Inductive Constructions
The Ackermann Award 2005
Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations
Model checking existential logic on partially ordered sets
Schema Mappings: Structural Properties and Limits (Invited Talk)
A Complete Inference System for Probabilistic Infinite Trace Equivalence
Compositional verification of termination-preserving refinement of concurrent programs
Semantic for Abstract Fairness using Metric Spaces
On the Minimisation of Deterministic and History-Deterministic Generalised (Co)Büchi Automata
Formulae-as-types for an involutive negation
Realizability Models for Large Cardinals
Unifying Büchi Complementation Constructions
Model Building by Resolution
The Lax Braided Structure of Streaming I/O
Arithmetic Circuits: An Overview (Invited Talk)
Towards Mechanized Program Verification with Separation Logic
Higher-Order Action Calculi
On Continuous Normalization
Logics with counting and equivalence
Degrees of Undecidability in Term Rewriting
A General Theorem on Termination of Rewriting
A Sequent Calculus for Circumscription
Pure Pointer Programs with Iteration
Continuous Fragment of the mu-Calculus
Functorial Boxes in String Diagrams
Pebble Games on Trees
Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time
Inductive and Functional Types in Ludics
The Height of Piecewise-Testable Languages with Applications in Logical Complexity
μ-Calculi with Atoms (Invited Talk)
Composition and Submachine Concepts for Sequential ASMs
Canonical Models and the Complexity of Modal Team Logic
Coherence by Normalization for Linear Multicategorical Structures
On Deciding Topological Classes of Deterministic Tree Languages
Comparing the Theory of Representations and Constructive Mathematics
The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter
Monadic NP and Built-in Trees
Logical Definability of NP-Optimization Problems with Monadic Auxiliary Predicates
Provability in TBLL: A Decision Procedure
The Ackermann award 2014
Not Enough Points Is Enough
Reasoning About States of Probabilistic Sequential Programs
On Existential Theories of List Concatenation
Provably Total Primitive Recursive Functions: Theories with Induction
Order-Invariant First-Order Logic over Hollow Trees
The Expressive Power of CSP-Quantifiers
High-Level Signatures and Initial Semantics
PDL with Intersection and Converse Is Decidable
Mathematical Structures in Dependent Type Theory (Invited Talk)
A Linear Logical View of Linear Type Isomorphisms
Classical and Intuitionistic Subexponential Logics Are Equally Expressive
Fibrational Induction Rules for Initial Algebras
Saturation-Based Model Checking of Higher-Order Recursion Schemes
Subtyping Functional+Nonempty Record Types
Computational Aspects of sigma-Definability over the Real Numbers without the Equality Test
One-Dimensional Logic over Words
Intersection, Universally Quantified, and Reference Types
Logical Aspects of Set Constraints
Unambiguity and uniformization problems on infinite trees
Full Abstraction for Resource Calculus with Tests
Typed Applicative Structures and Normalization by Evaluation for System F omega
Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction
Binding Forms in First-Order Logic
Closed Reductions in the lambda-Calculus
Choiceless Polynominal Time Computation and the Zero-One Law
Proofs in System F omega Can Be Done in System F omega 1
Energy and Mean-Payoff Games with Imperfect Information
Interfacing a Logic Machine
The Ackermann Award 2017
A Predicate Calculus with Control of Derivations
Is First Order Contained in an Initial Segment of PTIME?
Functions out of Higher Truncations
Structure Theorem and Strict Alternation Hierarchy for FO 2 on Words
Kripke Resource Models of a Dependently-Typed, Bunched lambda-Calculus
Equilibria of concurrent games on event structures
The Ackermann Award 2009
Resolution and the Weak Pigeonhole Principle
A Robust Class of Linear Recurrence Sequences
28th EACSL Annual Conference on Computer Science Logic, CSL 2020, Barcelona, Spain, January 13-16, 2020
Is Game Semantics Necessary?
Positive Deduction modulo Regular Theories
A Decidable Intuitionistic Temporal Logic
Logics For Context-Free Languages
A General Constructive Form of Higman's Lemma
Constraint-Based Analysis of Broadcast Protocols
The Joy of String Diagrams
Ontology-Based Data Access and Constraint Satisfaction
Cut-free Display Calculi for Relation Algebras
A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic
Extending the Dolev-Yao Intruder for Analyzing an Unbounded Number of Sessions
Focusing the Inverse Method for Linear Logic
Realizing Continuity Using Stateful Computations
Relational Parametricity for Higher Kinds
Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices)
Logical Characterization of Bounded Query Classes II: Polynomial-Time Oracle Machines
25th EACSL Annual Conference on Computer Science Logic, CSL 2016, Marseille, France, August 29 - September 1, 2016
Preservation Theorems Through the Lens of Topology
Modular Semantics and Logics of Classes
No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete
Kleene Algebra with Tests: Completeness and Decidability
Comparing the Expressive Power of Well-Structured Transition Systems
Effective Strategies for Enumeration Games
The Structure of Interaction
An Algebraic Foundation for Higraphs
Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes
On the Parameterised Intractability of Monadic Second-Order Logic
Subclasses of Quantified Boolean Formulas
Building Decision Procedures in the Calculus of Inductive Constructions
Light Functional Interpretation
Gardening with the Pythia A Model of Continuity in a Dependent Setting
A Sound Metalogical Semantics for Input/Output Effects
Extension Preservation on Dense Graph Classes
On Proof Nets for Multiplicative Linear Logic with Units
On the Interpretation of Type Theory in Locally Cartesian Closed Categories
Finite Variable Counting Logics with Restricted Requantification
On Completeness for NP via Projection Translations
Res Publica: The Universal Model of Computation (Invited Talk)
Synthetic Mathematics for the Mechanisation of Computability Theory and Logic (Invited Talk)
Verification in Predicate Logic with Time: Algorithmic Questions
A Logic for Probability in Quantum Systems
Infinitary Queries and Their Asymptotic Probabilities I: Properties Definable in Transitive Closue Logic
Omega-Regular Half-Positional Winning Conditions
A Remark on Minimal Polynomials of Boolean Functions
Effective Quantifier Elimination over Real Closed Fields (Tutorial)
The Arithmetical Complexity of Dimension and Randomness
Rank Logic is Dead, Long Live Rank Logic!
Categories with Algebraic Structure
Faster Algorithms for Alternating Refinement Relations
Algorithms for Propositional Updates
Learning Concepts Described By Weight Aggregation Logic
27th EACSL Annual Conference on Computer Science Logic, CSL 2018, Birmingham, UK, September 4-7, 2018
Functional reactive types
Complete Problems for Higher Order Logics
A Non-Standard Semantics for Kahn Networks in Continuous Time
Actual Arithmetic and Feasibility
An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets
The Exact Hardness of Deciding Derivational and Runtime Complexity
Bounded Arithmetic and Descriptive Complexity
Axiomatizing Subtyped Delimited Continuations
Aleph1 and the Modal mu-Calculus
From Local to Global Optimality in Concurrent Parity Games
On the Computability of Region-Based Euclidean Logics
What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives
Hoare Logic in the Abstract
Recursion for Higher-Order Encodings
Linear Time Algorithms and NP-Complete Problems
Secure equilibria in weighted games
Axiomatizing proof tree concepts in Bounded Arithmetic
Frobenius Structures in Star-Autonomous Categories
Symmetric Computation (Invited Talk)
Coalgebraic Derivations in Logic Programming
Positive Games and Persistent Strategies
Embedding Deduction Modulo into a Prover
Using Fields and Explicit Substitutions to Implement Objects and Functions in a de Bruijn Setting
Quadratic Correctness Criterion for Non-commutative Logic
New Intuitionistic Logical Constants: Undecidability of the Conservativsness Problem
Non-Commutative First-Order Sequent Calculus
Extension Preservation in the Finite and Prefix Classes of First Order Logic
Refined Complexity Analysis of Cut Elimination
A Comparison of the Resolution Caculus and the Connection Method, and a new Calculus Generalizing Both Methods
Parameterized Model Checking of Ring-Based Message Passing Systems
Recursion Schemata for NCk
Machine Characterization of the Classes of the W-Hierarchy
Logic for communicating automata with parameterized topology
How to Implement First Order Formulas in Local Memory Machine Models
The Freedoms of Guarded Bisimulation
Bounded-Arity Hierarchies in Fixed-Point Logics
Pebble Games and Linear Equations
Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion
Order-Invariance in the Two-Variable Fragment of First-Order Logic
Reachability in Distributed Memory Automata
Dynamic Cantor Derivative Logic
Bijections between Partitions by Two-Directional Rewriting Techniques
Faster decision of first-order graph properties
Current Trends and New Perspectives for First-Order Model Checking (Invited Talk)
Expressivity Within Second-Order Transitive-Closure Logic
Program Complexity of Dynamic LTL Model Checking
Jumping Boxes
Learning Automata and Transducers: A Categorical Approach
Testing for Finite State Systems
Degrees of Ambiguity for Parity Tree Automata
Beta reduction is invariant, indeed
Computer Science Logic - 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, Bergen, Norway, September 12-15, 2011, Proceedings
Two-Variable Logic on 2-Dimensional Structures
Life without the Terminal Type
More Computation Power for a Denotational Semantics for First Order Logic
Gentzen-Systems for Propositional Temporal Logics
Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T
Effective interpolation and preservation in guarded logics
On the Effective Semantics of Nondeterministic, Nonmonotonic, Temporal Logic Databases
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics
A New Type Assignment for Strongly Normalizable Terms
Model Checking FO(R) over One-Counter Processes and beyond
Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings
On the characterization of models of H
Data Types, Infinity and Equality in System AF 2
A Fully Abstract Denotational Model for Observational Precongruence
Lower Bounds for Space in Resolution
Notes on Sconing and Relators
Model Transformations in Decidability Proofs for Monadic Theories
There Exist Some omega -Powers of Any Borel Rank
A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion
The Knowledge Representation Language L LILOG
Evidence for Fixpoint Logic
Distributed Control Flow with Classical Modal Logic
Games, Mobile Processes, and Functions
Randomisation and Derandomisation in Descriptive Complexity Theory
New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures
Internal Calculi for Separation Logics
Clemens Lautemann: 1951-2005 An Obituary
From Pebble Games to Tractability: An Ambidextrous Consistency Algorithm for Quantified Constraint Satisfaction
Morphisms and Partitions of V-sets
Relating Two Standard Notions of Secrecy
The Isomorphism Problem for omega -Automatic Trees
Deduction by Combining Semantic Tableaux and Integer Programming
My (Un)Favourite Things
Quantified Constraints: Algorithms and Complexity
From Programs to Games: Invariance and Safety for Bisimulation
LISA: A Specification Language Based on WS2S
One hierarchy spawns another: graph deconstructions and the complexity classification of conjunctive queries
Forcing and Type Theory
Semi-Unification and Generalizations of a Particularly Simple Form
Taylor expansion for Call-By-Push-Value
Towards a Proof System for Admissibility
Regular combinators for string transformations
Duality between Call-by-Name Recursion and Call-by-Value Iteration
The Algebras for Automatic Relations
Canonization for L k -equivalence is Hard
BV and Pomset Logic Are Not the Same
A Logic of Coequations
Classical Proofs via Basic Logic
Planar Realizability via Left and Right Applications
Collapsibility in Infinite-Domain Quantified Constraint Satisfaction
A Conjunctive Logical Characterization of Nondeterministic Linear Time
An Upper Bound for Minimal Resolution Refutations
Bounded Combinatory Logic
Computer-checked mathematics: a formal proof of the odd order theorem
An Effective Extension of the Wagner Hierarchy to Blind Counter Automata
Finite Model Theory and Proof Complexity Revisited: Distinguishing Graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus
Determinizing Discounted-Sum Automata
Quantitative Hennessy-Milner Theorems via Notions of Density
Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus
Fast Cut-Elimination by Projection
On the Expressive Power of Graph Logic
Independence: Logics and Concurrency
A Bounding Quantifier
The Basic Logic of Proofs
On Relative and Probabilistic Finite Counterability
Automated Generation of Analytic Calculi for Logics with Linearity
Two-Variable Logic with Two Order Relations - (Extended Abstract)
Type-Based Termination with Sized Products
Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, Austria, July 14 - 18, 2014
Polymorphic Game Semantics for Dynamic Binding
A Simple Ordinal Recursive Normalization of Gödel's T
Axiomatizing the Least Fixed Point Operation and Binary Supremum
Partial Elements and Recursion via Dominances in Univalent Type Theory
Languages and Logical Definability in Concurrency Monoids
On periodically iterated morphisms
Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk)
Trading Probability for Fairness
Canonical Forms for Data-Specifications
Isomorphisms of scattered automatic linear orders
Complete Categorical Equational Deduction
Determinacy of Infinite Games: Perspectives of the Algorithmic Approach (Invited Talk)
On Counting Generalized Colorings
Capture Complexity by Partition
The Produoidal Algebra of Process Decomposition
The Commuting V-Diagram
Definability in Games
The Descriptive Complexity of Parity Games
On Generalizations of Semi-terms of Particularly Simple Form
Categorical and Kripke Semantics for Constructive S4 Modal Logic
Approximating Fixpoints of Approximated Functions (Invited Talk)
Coercive Subtyping in Type Theory
A Curry-Howard Correspondence for Linear, Reversible Computation
Higher-Order Matching and Games
Gödel's Theorem Without Tears - Essential Incompleteness in Synthetic Computability
Markov's Principle for Propositional Type Theory