FSCD 2025: FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION

This page contains an index consisting of author-provided keywords.

2
2-categories	Categorical Continuation Semantics for Concurrency
A
abstract machines	The Cost of Skeletal Call-by-Need, Smoothly
abstract rewriting system	Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality
Anti-unification	Combining Generalization Algorithms in Regular Collapse-Free Theories
B
Bidirectional typing	What does it take to certify a conversion checker?
Böhm trees	Ohana trees and Taylor expansion for the λI-calculus
Büchi acceptance	Higher-Dimensional Automata : Extension to Infinite Tracks
C
call-by-need	The Cost of Skeletal Call-by-Need, Smoothly
call-by-push-value	Grading call-by-push-value, explicitly and implicitly
Call-by-value	An Innermost DP Framework for Constrained Higher-order Rewriting
categorical logic	Unifying Algebraic and Boolean Descriptive Complexity
Categorical Semantics	Functorial Models of Differential Linear Logic
category theory	Unifying Algebraic and Boolean Descriptive Complexity Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
Certified algorithms	What does it take to certify a conversion checker?
Classical logic	Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation
coherence	Coherent Tietze transformations of 1-polygraphs in homotopy type theory
coinductive types	Impredicative Encodings of Inductive and Coinductive Types
Combination	Combining Generalization Algorithms in Regular Collapse-Free Theories
Combinatory algebras	From Partial to Monadic: Combinatory Algebra with Effects
commutative algebra	Unifying Algebraic and Boolean Descriptive Complexity
Compositional Semantics	An Expressive Trace Logic for Recursive Programs
Compositional Verification	An Expressive Trace Logic for Recursive Programs
Computational duality	Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation
computational effect	Grading call-by-push-value, explicitly and implicitly
Computational effects	From Partial to Monadic: Combinatory Algebra with Effects Quantitative Types for the Functional Machine Calculus
concurrency	Categorical Continuation Semantics for Concurrency
concurrency theory	Higher-Dimensional Automata : Extension to Infinite Tracks
confluence	Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality
constructive logic	A Zoo of Continuity Properties in Constructive Type Theory
Constructive Mathematics	Internal Effectful Forcing in System T A Zoo of Continuity Properties in Constructive Type Theory
continuations	Categorical Continuation Semantics for Concurrency
Continuity	Internal Effectful Forcing in System T A Zoo of Continuity Properties in Constructive Type Theory
Coq	A Zoo of Continuity Properties in Constructive Type Theory Mechanized Undecidability of Higher-order beta-Matching
Craig interpolation	Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation
Cut elimination	Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation
Cut introduction	Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation
D
Decidability	Knowledge Problems vs Unification and Matching: Dichotomy Results
decreasing diagrams method	Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality
denotational semantics	Categorical Continuation Semantics for Concurrency An Expressive Trace Logic for Recursive Programs
Dependency pairs	An Innermost DP Framework for Constrained Higher-order Rewriting
Dependent type theory	What does it take to certify a conversion checker?
descriptive complexity theory	Unifying Algebraic and Boolean Descriptive Complexity
Differentiable Programming	Functorial Models of Differential Linear Logic
differential logical relations	On the Metric Nature of (Differential) Logical Relations
Domain Equations	Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
E
effect system	Grading call-by-push-value, explicitly and implicitly
Effectful forcing	Internal Effectful Forcing in System T
Equational theories	Combining Generalization Algorithms in Regular Collapse-Free Theories The Unification Type of an Equational Theory May Depend on the Instantiation Preorder
Evidenced frames	From Partial to Monadic: Combinatory Algebra with Effects
F
Fixed Points	Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
Fixed-point Logic	An Expressive Trace Logic for Recursive Programs
formal proof	Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality
formulas-as-types	Impredicative Encodings of Inductive and Coinductive Types
fully lazy sharing	The Cost of Skeletal Call-by-Need, Smoothly
G
game semantics	Categorical Continuation Semantics for Concurrency
Generalization	Combining Generalization Algorithms in Regular Collapse-Free Theories
graded monad	Grading call-by-push-value, explicitly and implicitly
Graph Theory	Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
Guarded Fixed Points	Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
H
higher-dimensional automata	Higher-Dimensional Automata : Extension to Infinite Tracks
Higher-order logic	Monad Translations for Higher-Order Logic
higher-order matching	Mechanized Undecidability of Higher-order beta-Matching
Higher-order term rewriting	An Innermost DP Framework for Constrained Higher-order Rewriting
homotopy type theory	Coherent Tietze transformations of 1-polygraphs in homotopy type theory
I
implicit complexity	Branch Sequentialization in Quantum Polytime
impredicative types	Impredicative Encodings of Inductive and Coinductive Types
inductive types	Impredicative Encodings of Inductive and Coinductive Types
Innermost termination	An Innermost DP Framework for Constrained Higher-order Rewriting
Instantiation preorder	The Unification Type of an Equational Theory May Depend on the Instantiation Preorder
interactive theorem provers	A Zoo of Continuity Properties in Constructive Type Theory
intersection types	Quantitative Types for the Functional Machine Calculus
interval pomsets	Higher-Dimensional Automata : Extension to Infinite Tracks
Intuitionistic logic	Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation Monad Translations for Higher-Order Logic
K
Knowledge Problems	Knowledge Problems vs Unification and Matching: Dichotomy Results
Kuroda's translation	Monad Translations for Higher-Order Logic
L
lambda calculus	The Cost of Skeletal Call-by-Need, Smoothly
lambda-calculus	On the Metric Nature of (Differential) Logical Relations Ohana trees and Taylor expansion for the λI-calculus Quantitative Types for the Functional Machine Calculus Mechanized Undecidability of Higher-order beta-Matching
lambda-I-calculus	Ohana trees and Taylor expansion for the λI-calculus
lambda-theories	Ohana trees and Taylor expansion for the λI-calculus
Linear Logic	Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation Linear logic using negative connectives Functorial Models of Differential Linear Logic ∞-categorical models of linear logic
linear-non-linear adjunction	∞-categorical models of linear logic
Logical relations	Substructural Parametricity
Logically constrained term rewriting	An Innermost DP Framework for Constrained Higher-order Rewriting
M
Matching	Knowledge Problems vs Unification and Matching: Dichotomy Results
mechanization	Mechanized Undecidability of Higher-order beta-Matching
Modal and Description Logics	The Unification Type of an Equational Theory May Depend on the Instantiation Preorder
Monad	Monad Translations for Higher-Order Logic
Monads	From Partial to Monadic: Combinatory Algebra with Effects
Muller acceptance	Higher-Dimensional Automata : Extension to Infinite Tracks
multifocused proofs	Linear logic using negative connectives
O
omega pomsets	Higher-Dimensional Automata : Extension to Infinite Tracks
Ordered logic	Substructural Parametricity
Ordinals	Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
P
partial metric spaces	On the Metric Nature of (Differential) Logical Relations
polygraph	Coherent Tietze transformations of 1-polygraphs in homotopy type theory
polynomial time	Branch Sequentialization in Quantum Polytime
pomsets with interfaces	Higher-Dimensional Automata : Extension to Infinite Tracks
Presheaves	Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
program approximation	Ohana trees and Taylor expansion for the λI-calculus
Program Specification	An Expressive Trace Logic for Recursive Programs
Proof assistants	A Zoo of Continuity Properties in Constructive Type Theory
Proof Net	Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
Q
quantales	On the Metric Nature of (Differential) Logical Relations
quantum programming language	Branch Sequentialization in Quantum Polytime
quasi-metric spaces	On the Metric Nature of (Differential) Logical Relations
R
Realizability	From Partial to Monadic: Combinatory Algebra with Effects
reasonable cost models	The Cost of Skeletal Call-by-Need, Smoothly
resource calculus	Ohana trees and Taylor expansion for the λI-calculus
Rewriting	Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Rocq	Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It A Zoo of Continuity Properties in Constructive Type Theory
S
Semantics	Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Semirings	Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
sequent calculus	Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation Linear logic using negative connectives
Sequentialization	Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
simple types	Mechanized Undecidability of Higher-order beta-Matching
spectrum	∞-categorical models of linear logic
Substructural type systems	Substructural Parametricity
System L	Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation
System T	Internal Effectful Forcing in System T
T
Taylor expansion	Ohana trees and Taylor expansion for the λI-calculus
Termination	Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Tietze transformation	Coherent Tietze transformations of 1-polygraphs in homotopy type theory
Trace Logic	An Expressive Trace Logic for Recursive Programs
type theory	A Zoo of Continuity Properties in Constructive Type Theory
U
undecidability	Mechanized Undecidability of Higher-order beta-Matching
Unification	Knowledge Problems vs Unification and Matching: Dichotomy Results
Unification type	The Unification Type of an Equational Theory May Depend on the Instantiation Preorder
V
Verification	Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Y
Yeo's Theorem	Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
∞
∞-category	∞-categorical models of linear logic

Disclaimer | Powered by EasyChair Smart Program