FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

A
alpha-equivalence	Fixed-Point Constraints for Nominal Equational Unification
Anti-unification	Higher-Order Equational Pattern Anti-Unification Term-Graph Anti-Unification
automation	Completion for Logically Constrained Rewriting
B
B combinator	On repetitive right application of B-terms
Bimonad	Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
Böhm trees	Strict Ideal Completions of the Lambda Calculus
C
Categorical Quantum Mechanics	A diagrammatic axiomatisation of fermionic quantum circuits
category theory	Call-by-name Gradual Type Theory
Coalgebra Modality	Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
coherence	Coherence of Gray categories via rewriting
coinduction	Term rewriting characterisation of LOGSPACE for finite and infinite data
Combinatorics	Counting Environments and Closures
combinatory logic	On repetitive right application of B-terms
completeness	Completeness of Tree Automata Completion
completion	Completion for Logically Constrained Rewriting
complexity	Counting Environments and Closures
complexity classes	Unique perfect matchings and proof nets
conditional term rewriting	Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
confluence	Decreasing diagrams with two labels are complete for confluence of countable systems Confluence of Prefix-Constrained Rewrite Systems Strict Ideal Completions of the Lambda Calculus
constrained rewriting	Completion for Logically Constrained Rewriting
contractibility	Proof nets for bi-intuitionistic linear logic
Coq	Cumulative Inductive Types in Coq
correctness criteria	Unique perfect matchings and proof nets
critical pair	Confluence of Prefix-Constrained Rewrite Systems
cubical sets	Internal Universes in Models of Homotopy Type Theory
Cyclic term-graps	Term-Graph Anti-Unification
D
decreasing diagrams	Decreasing diagrams with two labels are complete for confluence of countable systems
denotational semantics	The clocks they are adjunctions. Denotational semantics for Clocked Type Theory Call-by-name Gradual Type Theory
dependent type theory	Internal Universes in Models of Homotopy Type Theory
E
Eilenberg-Moore Category	Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
Equational theories	Higher-Order Equational Pattern Anti-Unification Fixed-Point Constraints for Nominal Equational Unification
F
fermionic quantum computing	A diagrammatic axiomatisation of fermionic quantum circuits
fixed point equations	Fixed-Point Constraints for Nominal Equational Unification
functional programming	Nominal Unification with Atom and Context Variables Counting Environments and Closures
G
gradual typing	Call-by-name Gradual Type Theory
graph algorithms	Unique perfect matchings and proof nets
Gray category	Coherence of Gray categories via rewriting
Guarded Recursion	The clocks they are adjunctions. Denotational semantics for Clocked Type Theory
H
higher inductive types	A Syntax for Higher Inductive-Inductive Types
higher-order recursion schemes	Homogeneity without Loss of Generality
higher-order unification	Nominal Unification with Atom and Context Variables
homogeneous types	Homogeneity without Loss of Generality
homotopy type theory	A Syntax for Higher Inductive-Inductive Types Internal Universes in Models of Homotopy Type Theory
Hopf Monad	Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
I
implicit complexity	Term rewriting characterisation of LOGSPACE for finite and infinite data
Indexed types	Index-Stratified Types
Inductive Types	Cumulative Inductive Types in Coq
inductive-inductive types	A Syntax for Higher Inductive-Inductive Types
infinitary rewriting	Term rewriting characterisation of LOGSPACE for finite and infinite data Strict Ideal Completions of the Lambda Calculus
innermost conditional narrowing	Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
interactive tool	ProTeM: A Proof Term Manipulator
internal language	Internal Universes in Models of Homotopy Type Theory
intuitionistic linear logic	Proof nets for bi-intuitionistic linear logic
L
lambda calculus	Nominal Unification with Atom and Context Variables On repetitive right application of B-terms Strict Ideal Completions of the Lambda Calculus
lambda-calculus	Counting Environments and Closures Homogeneity without Loss of Generality
Least general generalization	Term-Graph Anti-Unification
Linear Category	Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
linear logic	Unique perfect matchings and proof nets Proof nets for bi-intuitionistic linear logic
logical relations	A Syntax for Higher Inductive-Inductive Types Index-Stratified Types
LOGSPACE	Term rewriting characterisation of LOGSPACE for finite and infinite data
M
mathematical analysis	Counting Environments and Closures
meaningless terms	Strict Ideal Completions of the Lambda Calculus
Mixed Distributive Law	Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
modalities	Internal Universes in Models of Homotopy Type Theory
monoidal categories	A diagrammatic axiomatisation of fermionic quantum circuits
Monoidal Coalgebra Modality	Lifting Coalgebra Modalities and IMELL Model Structure to Eilenberg-Moore Categories
N
nominal terms	Fixed-Point Constraints for Nominal Equational Unification
nominal unification	Nominal Unification with Atom and Context Variables Fixed-Point Constraints for Nominal Equational Unification
normalisation	Strict Ideal Completions of the Lambda Calculus
O
over-approximation	Completeness of Tree Automata Completion
P
polygraph	Coherence of Gray categories via rewriting
prefix-constrained term rewriting	Confluence of Prefix-Constrained Rewrite Systems
program transformation	Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
program transformations	Nominal Unification with Atom and Context Variables
proof assistants	Cumulative Inductive Types in Coq
Proof nets	Proof nets for bi-intuitionistic linear logic
proof terms	ProTeM: A Proof Term Manipulator
PSPACE	A Unifying Framework for Type Inhabitation
Q
Quantum Computing	A diagrammatic axiomatisation of fermionic quantum circuits
quotient inductive types	A Syntax for Higher Inductive-Inductive Types
R
Recursive types	Index-Stratified Types
regular tree grammar	Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems
regularity preservation	Completeness of Tree Automata Completion
rewriting	A Unifying Framework for Type Inhabitation Coherence of Gray categories via rewriting
S
safe schemes	Homogeneity without Loss of Generality
simple types	A Unifying Framework for Type Inhabitation
Simply typed lambda calculus	Higher-Order Equational Pattern Anti-Unification
string diagrams	A diagrammatic axiomatisation of fermionic quantum circuits
Subtyping	Cumulative Inductive Types in Coq
Systems of recursion equations	Term-Graph Anti-Unification
T
term rewriting	Term rewriting characterisation of LOGSPACE for finite and infinite data ProTeM: A Proof Term Manipulator
Term Rewriting Systems	Completeness of Tree Automata Completion
theorem proving	Completion for Logically Constrained Rewriting
tree automata	Completeness of Tree Automata Completion
tree automata completion	Completeness of Tree Automata Completion
type inhabitation	A Unifying Framework for Type Inhabitation
type theory	The clocks they are adjunctions. Denotational semantics for Clocked Type Theory Call-by-name Gradual Type Theory
U
univalent foundations	Internal Universes in Models of Homotopy Type Theory
Universes	Internal Universes in Models of Homotopy Type Theory Cumulative Inductive Types in Coq
W
weak diamond property	Decreasing diagrams with two labels are complete for confluence of countable systems
Z
zw calculus	A diagrammatic axiomatisation of fermionic quantum circuits
zx calculus	A diagrammatic axiomatisation of fermionic quantum circuits

Disclaimer | Powered by EasyChair Smart Program