FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

Disclaimer | Powered by EasyChair Smart Program