FSCD 2023: 8TH INTERNATIONAL CONFERENCE ON FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION 2023

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

$
$\infty$-logos	Homotopy type theory as internal languages of diagrams of $\infty$-logoses
$\infty$-topos	Homotopy type theory as internal languages of diagrams of $\infty$-logoses
A
Abstract guardedness	Representing Guardedness in Call-by-Value
abstract rewriting system	Generalized Newman's Lemma for Discrete and Continuous Systems
abstract syntax	E-unification for Second-Order Abstract Syntax
Administrative normal form	The logical essence of compiling with continuations
AI	How Can We Make Trustworthy AI?
Algebraic datatypes	Automata-based verification of relational properties of functions over data structures
arithmetic	Cyclic proofs for (arithmetical) inductive definitions
Artin gluing	Homotopy type theory as internal languages of diagrams of $\infty$-logoses
automated termination analysis	Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition
B
Bar recursion	Diller-Nahm bar recursion
battle of Hercules and Hydra	Hydra Battles and AC Termination
bicategory theory	The Formal Theory of Monads, Univalently
Binding operator	Nominal Techniques for Software Specification and Verification
Bounded Polymorphism	Dinaturality meets genericity: a game semantics of bounded polymorphism.
Bunched Implication logic	Labelled Tableaux for Linear Time Bunched Implication Logic
C
Calculus of relations	Quotients and Extensionality in Relational Doctrines
call-by-value semantics	Cost-Size Semantics for Call-by-Value Higher-Order Rewriting
canonicity	For the Metatheory of Type Theory, Internal Sconing Is Enough
cartesian categories	Rewriting modulo traced comonoid structure
Categorical semantics	Strategies as Resource Terms, and their Categorical Semantics
Categorification	Convolution Products on Double Categories and Categorification of Rule Algebras
coherence	Categorical coherence from term rewriting systems
coinduction	Cyclic proofs for (arithmetical) inductive definitions
Combinatory logic	Combinatory logic and lambda calculus are equal, algebraically
comonoid structure	Rewriting modulo traced comonoid structure
complexity	Cost-Size Semantics for Call-by-Value Higher-Order Rewriting
Compositional categorical rewriting theory	Convolution Products on Double Categories and Categorification of Rule Algebras
concurrent processes	Concurrent Realizability on Conjunctive Structures
confluence	Generalized Newman's Lemma for Discrete and Continuous Systems
Constrained Horn Clauses	Automata-based verification of relational properties of functions over data structures
Continuation-passing style	The logical essence of compiling with continuations
Convolution products	Convolution Products on Double Categories and Categorification of Rule Algebras
Coq	The Formal Theory of Monads, Univalently
Cubical Agda	Combinatory logic and lambda calculus are equal, algebraically
cyclic proofs	Cyclic proofs for (arithmetical) inductive definitions
D
denotational models	A Lambda Calculus Satellite
Denotational Semantics	Unifying Graded Linear Logic and Differential Operators The Sum-Product Algorithm for Quantitative Multiplicative Linear Logic
Dialectica	Diller-Nahm bar recursion
digital circuits	Rewriting modulo traced comonoid structure
Diller-Nahm	Diller-Nahm bar recursion
Dinaturality	Dinaturality meets genericity: a game semantics of bounded polymorphism.
discrete-continuous systems	Generalized Newman's Lemma for Discrete and Continuous Systems
Double categories	Convolution Products on Double Categories and Categorification of Rule Algebras
double pushout rewriting	Rewriting modulo traced comonoid structure
E
Elgot iteration	Representing Guardedness in Call-by-Value
equational theories	Nominal Techniques for Software Specification and Verification A Lambda Calculus Satellite
equational unification	E-unification for Second-Order Abstract Syntax
F
Fine-grain call-by-value	Representing Guardedness in Call-by-Value
fixed points	Cyclic proofs for (arithmetical) inductive definitions
formal proof	Generalized Newman's Lemma for Discrete and Continuous Systems
Formal verification	Automata-based verification of relational properties of functions over data structures
formalization	The Formal Theory of Monads, Univalently
Freyd category	Representing Guardedness in Call-by-Value
Functional Analysis	Unifying Graded Linear Logic and Differential Operators
G
Game Semantics	Dinaturality meets genericity: a game semantics of bounded polymorphism. Strategies as Resource Terms, and their Categorical Semantics
Generalized applications	The logical essence of compiling with continuations
geometry of interaction	On the Lattice of Program Metrics
gluing	For the Metatheory of Type Theory, Internal Sconing Is Enough
Graded Logic	Unifying Graded Linear Logic and Differential Operators
graph rewriting	Rewriting modulo traced comonoid structure
groupoid	Categorical coherence from term rewriting systems
H
higher-order rewriting	Cost-Size Semantics for Call-by-Value Higher-Order Rewriting
higher-order unification	E-unification for Second-Order Abstract Syntax
Homotopy type theory	Homotopy type theory as internal languages of diagrams of $\infty$-logoses
human-centric computing	How Can We Make Trustworthy AI?
Hyperdoctrines	Quotients and Extensionality in Relational Doctrines
hypergraphs	Rewriting modulo traced comonoid structure
I
inductive definitions	Cyclic proofs for (arithmetical) inductive definitions
intersection types	A quantitative version of simple types
Isabelle formalization	Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition
K
Kleisli category	Representing Guardedness in Call-by-Value
knowledge representation	How Can We Make Trustworthy AI?
L
Labelled deduction	Labelled Tableaux for Linear Time Bunched Implication Logic
lambda calculus	Combinatory logic and lambda calculus are equal, algebraically Two Decreasing Measures for Simply Typed Lambda-Terms A Lambda Calculus Satellite
lambda-calculus	A quantitative version of simple types On the Lattice of Program Metrics
Linear Logic	Concurrent Realizability on Conjunctive Structures Type Isomorphisms for Multiplicative Additive Linear Logic Unifying Graded Linear Logic and Differential Operators The Sum-Product Algorithm for Quantitative Multiplicative Linear Logic
Linear temporal logic LTL	Partial model checking and partial model synthesis in LTL using a tableau-based approach
logical relation	Homotopy type theory as internal languages of diagrams of $\infty$-logoses
M
machine learning	How Can We Make Trustworthy AI?
metamathematics	Cyclic proofs for (arithmetical) inductive definitions
metric preservation	On the Lattice of Program Metrics
Metric spaces	Quotients and Extensionality in Relational Doctrines
modality	Homotopy type theory as internal languages of diagrams of $\infty$-logoses
Model inference	Automata-based verification of relational properties of functions over data structures
monads	The Formal Theory of Monads, Univalently
monoidal theories	Rewriting modulo traced comonoid structure
Multiplicative Additive fragment	Type Isomorphisms for Multiplicative Additive Linear Logic
N
Nominal Logic	Nominal Techniques for Software Specification and Verification
Nominal Rewriting	Nominal Techniques for Software Specification and Verification
normalization	For the Metatheory of Type Theory, Internal Sconing Is Enough
O
oplax limit	Homotopy type theory as internal languages of diagrams of $\infty$-logoses
P
parallelism	Concurrent Realizability on Conjunctive Structures
partial model checking	Partial model checking and partial model synthesis in LTL using a tableau-based approach
partial model synthesis	Partial model checking and partial model synthesis in LTL using a tableau-based approach
partial transition systems	Partial model checking and partial model synthesis in LTL using a tableau-based approach
presheaves	For the Metatheory of Type Theory, Internal Sconing Is Enough
Probabilistic Programming	The Sum-Product Algorithm for Quantitative Multiplicative Linear Logic
processes with fusions	Concurrent Realizability on Conjunctive Structures
program metrics	On the Lattice of Program Metrics
proof assistant	Generalized Newman's Lemma for Discrete and Continuous Systems
Proof nets	Type Isomorphisms for Multiplicative Additive Linear Logic
proof theory	Cyclic proofs for (arithmetical) inductive definitions
Proof-Nets	The Sum-Product Algorithm for Quantitative Multiplicative Linear Logic
Q
Quantitative reasoning	Quotients and Extensionality in Relational Doctrines
quotient inductive types	Combinatory logic and lambda calculus are equal, algebraically
R
realizability	Concurrent Realizability on Conjunctive Structures
reasoning	How Can We Make Trustworthy AI?
Relational properties	Automata-based verification of relational properties of functions over data structures
Resource calculus	Strategies as Resource Terms, and their Categorical Semantics
rewriting	Categorical coherence from term rewriting systems Two Decreasing Measures for Simply Typed Lambda-Terms A Lambda Calculus Satellite
Rule algebras	Convolution Products on Double Categories and Categorification of Rule Algebras
S
sconing	For the Metatheory of Type Theory, Internal Sconing Is Enough
security protocols	Knowledge Problems in Security Protocols: Going Beyond Subterm-Convergent Theories
Sequent calculus	Type Isomorphisms for Multiplicative Additive Linear Logic The logical essence of compiling with continuations
Simple Types	Two Decreasing Measures for Simply Typed Lambda-Terms
Strong Normalization	Two Decreasing Measures for Simply Typed Lambda-Terms
Subtyping	Dinaturality meets genericity: a game semantics of bounded polymorphism.
symmetric traced monoidal categories	Rewriting modulo traced comonoid structure
synthetic Tait computability	Homotopy type theory as internal languages of diagrams of $\infty$-logoses
T
tableaux	Partial model checking and partial model synthesis in LTL using a tableau-based approach
Tableaux calculus	Labelled Tableaux for Linear Time Bunched Implication Logic
Temporal logic	Labelled Tableaux for Linear Time Bunched Implication Logic
term rewriting	Knowledge Problems in Security Protocols: Going Beyond Subterm-Convergent Theories Hydra Battles and AC Termination Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition
termination	Hydra Battles and AC Termination Two Decreasing Measures for Simply Typed Lambda-Terms Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition
Tree automata	Automata-based verification of relational properties of functions over data structures
Type Isomorphisms	Type Isomorphisms for Multiplicative Additive Linear Logic
Type System	Nominal Techniques for Software Specification and Verification
type theory	For the Metatheory of Type Theory, Internal Sconing Is Enough
U
undecidability	α-avoidance
unification	A quantitative version of simple types Nominal Techniques for Software Specification and Verification
univalent foundations	The Formal Theory of Monads, Univalently
V
variable capture	α-avoidance
verification	Knowledge Problems in Security Protocols: Going Beyond Subterm-Convergent Theories
α
α-conversion	α-avoidance
λ
λ-calculus	α-avoidance

Disclaimer | Powered by EasyChair Smart Program