FSCD 2020: INTERNATIONAL CONFERENCE ON FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION

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

2
2-categories	Comprehension and quotient structures in the language of 2-categories
A
Agda	A Syntax for Mutual Inductive Families
algebraic effect	A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers
Algebraic Hierarchy	Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi - System description
Anti-unification	Unital Anti-unification: Type and Algorithms
arithmetic	Adventures in Verifying Arithmetic
Atomicity	Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
automatic analysis	WANDA - a Higher Order Termination Tool - System description
Average-case complexity	On Average-Case Hardness of Higher-Order Model Checking
B
bar recursion	A Gentzen-style monadic translation of Goedel's System T
behavioral equivalence	A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers
Binary fuzzy relations	Constraint Solving over Multiple Similarity Relations
bisimilarity	A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers
Bunched logic	Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
C
call-by-value lambda calculus	A Reflection on Continuation-Composing Style
Cartesian difference categories	The difference lambda-calculus: a language for difference categories.
Cartesian differential categories	The difference lambda-calculus: a language for difference categories.
categories of algebras and coalgebras	Comprehension and quotient structures in the language of 2-categories
category theory	String diagrams for optics Modules over monads and operational semantics Conditional Bisimilarity for Reactive Systems
certification	Certifying Termination Proofs: From Term Rewriting to SMT Solving and Back
Change actions	The difference lambda-calculus: a language for difference categories.
collapse theories	Unital Anti-unification: Type and Algorithms
complexity	Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars
Comprehension categories	Comprehension and quotient structures in the language of 2-categories
Comprehension structures	Comprehension and quotient structures in the language of 2-categories
Comprehension structures with image	Comprehension and quotient structures in the language of 2-categories
Comprehension structures with section	Comprehension and quotient structures in the language of 2-categories
computational lambda calculus	A Reflection on Continuation-Composing Style
Concurrency	Semi-Axiomatic Sequent Calculus
Concurrent Kleene Algebra	Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
conditional bisimilarity	Conditional Bisimilarity for Reactive Systems
constraint solving	Constraint Solving over Multiple Similarity Relations
Constructive Logic	Refining Constructive Hybrid Games
continuation-passing style	A Reflection on Continuation-Composing Style
continuity	A Gentzen-style monadic translation of Goedel's System T
Coq	Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi - System description
D
D-categories	Comprehension and quotient structures in the language of 2-categories
data-flow analysis	Data-flow analyses as effects and graded monads
decidability	A Probabilistic Higher-order Fixpoint Logic
decision procedure	A Fast Decision Procedure for Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems
decision trees	The new rewriting engine of Dedukti - System description
delimited control	A Reflection on Continuation-Composing Style
Delta-framework	A Type Checker for a Logical Framework with Union and Intersection Types - System description
dependency pair framework	WANDA - a Higher Order Termination Tool - System description
dependent type theory	Quotients in Dependent Type Theory
dependent types	Encoding Agda Programs using Rewriting A Type Checker for a Logical Framework with Union and Intersection Types - System description Type safety of rewriting rules in dependent types
Difference lambda-calculus	The difference lambda-calculus: a language for difference categories.
Differential lambda-calculus	The difference lambda-calculus: a language for difference categories.
E
effect systems	Data-flow analyses as effects and graded monads
Elpi	Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi - System description
Eta-conversion	Encoding Agda Programs using Rewriting
Extensionality	Encoding Agda Programs using Rewriting
F
Frame rules	Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
G
Game Logic	Refining Constructive Hybrid Games
Game Semantics	Symbolic Execution Game Semantics
Goedel's System T	A Gentzen-style monadic translation of Goedel's System T
graded monads	Data-flow analyses as effects and graded monads
graph transformation	Conditional Bisimilarity for Reactive Systems
H
handler	A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers
Higher inductive inductive types	Towards Constructive Hybrid Semantics
higher-order grammar	Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars
higher-order logic	Efficient Full Higher-Order Unification *** Best paper by junior researchers
Higher-order model checking	On Average-Case Hardness of Higher-Order Model Checking
Higher-Order Open Programs	Symbolic Execution Game Semantics
higher-order recursive path ordering	WANDA - a Higher Order Termination Tool - System description
higher-order rewriting	The new rewriting engine of Dedukti - System description
higher-order term rewriting	WANDA - a Higher Order Termination Tool - System description
HOL	Adventures in Verifying Arithmetic
Hybrid Games	Refining Constructive Hybrid Games
Hybrid semantics	Towards Constructive Hybrid Semantics
I
indexing data structures	Efficient Full Higher-Order Unification *** Best paper by junior researchers
inductive types	A Syntax for Mutual Inductive Families
Intensional type theory	Towards Constructive Hybrid Semantics
Intersection type system	On Average-Case Hardness of Higher-Order Model Checking
Intersection Types	A Type Checker for a Logical Framework with Union and Intersection Types - System description A foundational lambda calculus for probabilistic computation
Intuitionistic logic	Semi-Axiomatic Sequent Calculus
Isabelle/HOL	Certifying Termination Proofs: From Term Rewriting to SMT Solving and Back
K
Knuth-Bendix completion	Type safety of rewriting rules in dependent types
L
Lambda Calculus	A foundational lambda calculus for probabilistic computation
Language-integrated query	Strongly Normalizing Higher-Order Relational Queries
Lawvere categories	Comprehension and quotient structures in the language of 2-categories
lens	String diagrams for optics
Linear Logic	A Profunctorial Scott Semantics
Local reasoning	Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
Logical Framework	Encoding Agda Programs using Rewriting
logical relation	A Gentzen-style monadic translation of Goedel's System T
M
majorizability	A Gentzen-style monadic translation of Goedel's System T
mechanization	Undecidability of Semi-unification on a Napkin *** Best paper by a junior researcher
Metaprogramming	Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi - System description A Modal Analysis of Metaprogramming
Modal Type System	A Modal Analysis of Metaprogramming
model checking problem	A Probabilistic Higher-order Fixpoint Logic
Modules over monads	Modules over monads and operational semantics
monadic translation	A Gentzen-style monadic translation of Goedel's System T
monads	Data-flow analyses as effects and graded monads
mutual inductive types	A Syntax for Mutual Inductive Families
N
negative translation	A Gentzen-style monadic translation of Goedel's System T
Nested relational calculus	Strongly Normalizing Higher-Order Relational Queries
O
Operational semantics	Modules over monads and operational semantics
optic	String diagrams for optics
P
Packed Classes	Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi - System description
pattern matching	Adaptive Non-linear Pattern Matching Automata The new rewriting engine of Dedukti - System description
Pomsets	Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
Probabilistic Computation	A foundational lambda calculus for probabilistic computation
probabilistic logics	A Probabilistic Higher-order Fixpoint Logic
Profunctors	A Profunctorial Scott Semantics
Proof theory	Semi-Axiomatic Sequent Calculus
Q
quotient	Quotients in Dependent Type Theory
quotient inductive type	Quotients in Dependent Type Theory
Quotient structures	Comprehension and quotient structures in the language of 2-categories
R
reactive systems	Conditional Bisimilarity for Reactive Systems
reasoning by induction and coinduction	Comprehension and quotient structures in the language of 2-categories
reduction order	Certifying Termination Proofs: From Term Rewriting to SMT Solving and Back
Refinement	Refining Constructive Hybrid Games
refinement types	Resource-Aware Session Types with Arithmetic Refinements *** Best system description by a junior researcher
refiner	A Type Checker for a Logical Framework with Union and Intersection Types - System description
reflection	A Reflection on Continuation-Composing Style
resource analysis	Resource-Aware Session Types with Arithmetic Refinements *** Best system description by a junior researcher
rewriting	Encoding Agda Programs using Rewriting Type safety of rewriting rules in dependent types
S
Scott Semantics	A Profunctorial Scott Semantics
Semantics	Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
semi-unification	Undecidability of Semi-unification on a Napkin *** Best paper by a junior researcher
Separation	Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
Sequent calculus	Semi-Axiomatic Sequent Calculus
session types	Resource-Aware Session Types with Arithmetic Refinements *** Best system description by a junior researcher
shallow term rewriting systems	A Fast Decision Procedure for Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems
similarity relations	Constraint Solving over Multiple Similarity Relations
Solvability	A foundational lambda calculus for probabilistic computation
Species	A Profunctorial Scott Semantics
string diagram	String diagrams for optics
Strong normalization	Strongly Normalizing Higher-Order Relational Queries
subject-reduction	Type safety of rewriting rules in dependent types
subtyping	A Type Checker for a Logical Framework with Union and Intersection Types - System description
Symbolic Execution	Symbolic Execution Game Semantics
systems	Quotients in Dependent Type Theory
T
Term indexing	Adaptive Non-linear Pattern Matching Automata
term rewriting	Efficient Full Higher-Order Unification *** Best paper by junior researchers
termination	WANDA - a Higher Order Termination Tool - System description
termination analysis	Certifying Termination Proofs: From Term Rewriting to SMT Solving and Back
theorem proving	Efficient Full Higher-Order Unification *** Best paper by junior researchers
theorem-proving	Quotients in Dependent Type Theory
Tree automata	Adaptive Non-linear Pattern Matching Automata
tree grammars	Unital Anti-unification: Type and Algorithms
tree language	Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars
TT-lifting	Strongly Normalizing Higher-Order Relational Queries
type checker	A Type Checker for a Logical Framework with Union and Intersection Types - System description
type systems	Resource-Aware Session Types with Arithmetic Refinements *** Best system description by a junior researcher A Modal Analysis of Metaprogramming
Type theory	Encoding Agda Programs using Rewriting A Syntax for Mutual Inductive Families
type-checking	Type safety of rewriting rules in dependent types
U
undecidability	Undecidability of Semi-unification on a Napkin *** Best paper by a junior researcher
unification	Efficient Full Higher-Order Unification *** Best paper by junior researchers
union types	A Type Checker for a Logical Framework with Union and Intersection Types - System description
uniqueness of normal forms w.r.t. conversion	A Fast Decision Procedure for Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems
unital theories	Unital Anti-unification: Type and Algorithms
Universe polymorphism	Encoding Agda Programs using Rewriting
up-to context	Conditional Bisimilarity for Reactive Systems
Useless analysis	On Average-Case Hardness of Higher-Order Model Checking
V
verification	Adventures in Verifying Arithmetic
W
W-types	A Syntax for Mutual Inductive Families
word language	Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars
Y
Yoneda lemma	String diagrams for optics
Z
Zeno behaviour	Towards Constructive Hybrid Semantics
λ
λProlog	Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi - System description

Disclaimer | Powered by EasyChair Smart Program