FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

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

A
abstract rewriting	Strategies for Asymptotic Normalization
AC-Unification	A Certified Algorithm for AC-Unification
Agda	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities Division by two, in homotopy type theory
Algebra Interpretations	Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting
anti-unification	Nominal Anti-Unification with Atom-Variables
Artin gluing	Sheaf semantics of termination-insensitive noninterference
Automatic Complexity Analysis	mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
axiom of choice	Division by two, in homotopy type theory
B
Backreferences	On Lookaheads in Regular Expressions with Backreferences
Bicategories	A combinatorial approach to higher-order structure for polynomial functors
C
Call-by-name	Solvability for Generalized Applications
call-by-push-value	Galois connecting call-by-value and call-by-name
Call-by-value	Solvability for Generalized Applications
canonicity	A stratified approach to Lob induction
Categorical models	A combinatorial approach to higher-order structure for polynomial functors
categorical semantics	Galois connecting call-by-value and call-by-name
Certified Algorithms	A Certified Algorithm for AC-Unification
Choice sequences	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
Church's thesis	An Analysis of Tennenbaum's Theorem in Constructive Type Theory
Circular proofs	Decision problems for linear logic with least and greatest fixed points
Classical Logic	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
Combination Problem	Combined Hierarchical Matching: The Regular Case
combinatorial proofs	Normalization without syntax
combinatory logic	On Quantitative Algebraic Higher-Order Theories
computability theory	Certified Decision Procedures for Two-Counter Machines
computational effect	Galois connecting call-by-value and call-by-name
concurrency	Type-Based Termination for Futures
confluence	Compositional Confluence Criteria
constructive mathematics	Certified Decision Procedures for Two-Counter Machines
constructive type theory	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities An Analysis of Tennenbaum's Theorem in Constructive Type Theory
Coq	Certified Decision Procedures for Two-Counter Machines An Analysis of Tennenbaum's Theorem in Constructive Type Theory
counter automata	Certified Decision Procedures for Two-Counter Machines
Curry-Howard correspondence	Normalization without syntax
Cut Elimination	A Graphical Proof Theory of Logical Time
D
decidability	Certified Decision Procedures for Two-Counter Machines
decreasing diagrams	Compositional Confluence Criteria
Dedukti	Adequate and computational encodings in the logical framework Dedukti
deep inference	A Graphical Proof Theory of Logical Time A Methodology for Designing Proof Search Calculi for Non-Classical Logics
Denotational semantics	A combinatorial approach to higher-order structure for polynomial functors Sheaf semantics of termination-insensitive noninterference
Dependency Pairs	Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting
dependent type theory	A stratified approach to Lob induction
Diagrammatic language	Addition and differentiation of ZX-diagrams
Display calculus	A Methodology for Designing Proof Search Calculi for Non-Classical Logics
distributive laws	Stateful Structural Operational Semantics
division	Division by two, in homotopy type theory
E
emptiness	Restricting tree grammars with term rewriting
evaluation order	Galois connecting call-by-value and call-by-name
Extensional Type Theory	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
F
fibrations	A Fibrational Tale of Operational Logical Relations
finiteness	Restricting tree grammars with term rewriting
first-order logic	An Analysis of Tennenbaum's Theorem in Constructive Type Theory
fixed points	Decision problems for linear logic with least and greatest fixed points
formal methods	A Certified Algorithm for AC-Unification
futures	Type-Based Termination for Futures
G
generalisation	Nominal Anti-Unification with Atom-Variables
Generalized applications	Solvability for Generalized Applications
generic effects	A Fibrational Tale of Operational Logical Relations
gluing	A stratified approach to Lob induction
Guarded Recursion	A stratified approach to Lob induction
H
higher-order deduction	Nominal Anti-Unification with Atom-Variables
higher-order term rewriting	Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting
homotopy type theory	Division by two, in homotopy type theory
I
Implicit Computational Complexity	mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
infinite proofs	Type-Based Termination for Futures
information flow	Sheaf semantics of termination-insensitive noninterference
Interactive Theorem Proving	A Certified Algorithm for AC-Unification
Intuitionism	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
intuitionistic logic	Normalization without syntax
L
lambda calculus	Linear lambda-calculus is linear On Quantitative Algebraic Higher-Order Theories
lambda-calculus	Strategies for Asymptotic Normalization Solvability for Generalized Applications Normalization without syntax
Law of Excluded Middle	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
linear logic	Linear lambda-calculus is linear Decision problems for linear logic with least and greatest fixed points
lob induction	A stratified approach to Lob induction
logical framework	Encoding type universes without using matching modulo associativity and commutativity
logical frameworks	Adequate and computational encodings in the logical framework Dedukti
logical relations	A Fibrational Tale of Operational Logical Relations
Lookaheads	On Lookaheads in Regular Expressions with Backreferences
M
Matching	Combined Hierarchical Matching: The Regular Case
matching modulo AC	Encoding type universes without using matching modulo associativity and commutativity
mechanization	Certified Decision Procedures for Two-Counter Machines
Memory automata	On Lookaheads in Regular Expressions with Backreferences
metric spaces	On Quantitative Algebraic Higher-Order Theories
modal type theory	Sheaf semantics of termination-insensitive noninterference A stratified approach to Lob induction
modularity	Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting
monoidal closed categories	Rewriting for monoidal closed categories
N
Nested sequent calculus	A Methodology for Designing Proof Search Calculi for Non-Classical Logics
nominal algorithms	Nominal Anti-Unification with Atom-Variables
noninterference	Sheaf semantics of termination-insensitive noninterference
normalization	Restricting tree grammars with term rewriting Strategies for Asymptotic Normalization
O
operational semantics	A Fibrational Tale of Operational Logical Relations
P
Peano arithmetic	An Analysis of Tennenbaum's Theorem in Constructive Type Theory
phase distinction	Sheaf semantics of termination-insensitive noninterference
Polynomial functors	A combinatorial approach to higher-order structure for polynomial functors
polynomial termination	Polynomial Termination over N is Undecidable
probabilistic lambda-calculus	Strategies for Asymptotic Normalization
probabilistic rewriting	Strategies for Asymptotic Normalization
program distance	A Fibrational Tale of Operational Logical Relations
Program Verification	mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
proof nets	Normalization without syntax
proof theory	Linear lambda-calculus is linear A Graphical Proof Theory of Logical Time A Methodology for Designing Proof Search Calculi for Non-Classical Logics
Pure Type Systems	Adequate and computational encodings in the logical framework Dedukti
PVS	A Certified Algorithm for AC-Unification
Q
quantitative algebras	On Quantitative Algebraic Higher-Order Theories
Quantitative types	Solvability for Generalized Applications
Quantum Computation	Addition and differentiation of ZX-diagrams
Quantum Computing	Linear lambda-calculus is linear
R
Realizability	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
References	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
Regular expressions	On Lookaheads in Regular Expressions with Backreferences
Regular Theories	Combined Hierarchical Matching: The Regular Case
rewriting	Adequate and computational encodings in the logical framework Dedukti Encoding type universes without using matching modulo associativity and commutativity Rewriting for monoidal closed categories
rule formats	Stateful Structural Operational Semantics
S
Sequent Calculus	A Methodology for Designing Proof Search Calculi for Non-Classical Logics
sequentiality	A Graphical Proof Theory of Logical Time
series-parallel orders	A Graphical Proof Theory of Logical Time
set theory	Division by two, in homotopy type theory
sized types	Type-Based Termination for Futures
Solvability	Solvability for Generalized Applications
Species of structures	A combinatorial approach to higher-order structure for polynomial functors
Static Program Analysis	mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
strategies	Strategies for Asymptotic Normalization
string diagrams	Rewriting for monoidal closed categories
Structural operational semantics	Stateful Structural Operational Semantics
synthetic computability	An Analysis of Tennenbaum's Theorem in Constructive Type Theory
Synthetic domain theory	Sheaf semantics of termination-insensitive noninterference
synthetic Tait computability	Sheaf semantics of termination-insensitive noninterference
T
Tennenbaum's theorem	An Analysis of Tennenbaum's Theorem in Constructive Type Theory
term rewriting	Polynomial Termination over N is Undecidable Restricting tree grammars with term rewriting Compositional Confluence Criteria
Termination	Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting Polynomial Termination over N is Undecidable
theorem proving	Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
topos theory	Sheaf semantics of termination-insensitive noninterference
tree automata	Restricting tree grammars with term rewriting
tree grammar	Restricting tree grammars with term rewriting
type theory	Adequate and computational encodings in the logical framework Dedukti Encoding type universes without using matching modulo associativity and commutativity
type universes	Encoding type universes without using matching modulo associativity and commutativity
type-based termination	Type-Based Termination for Futures
U
Undecidability	Polynomial Termination over N is Undecidable Decision problems for linear logic with least and greatest fixed points
Z
ZX-calculus	Addition and differentiation of ZX-diagrams

Disclaimer | Powered by EasyChair Smart Program