Utilities and examples

Utilities for vectors

• Accessing a vector of length n with an element of I^n.
• Utilities for elements of I^n.
• Utilities for lists

Syntax for the rowing machines

• Custom induction for rows
• Modified Autosubst output

Modular syntax of types and terms

Polarized syntax with polyadic binders

• Syntax for types and contexts
• Custom induction for types
• Modified Autosubst output

General facts of Counter Machines as defined by Pierce

General facts of Counter Machines as defined in the Undecidability library

• Synthetic Undecidability

General facts of Rowing Machines

Unscoped syntax example

Well-scoped syntax example

Polyadic syntax example

Encoding of well-scoped syntax as unscoped syntax

Encoding of polyadic syntax as well-scoped syntax

Definitions

Counter machine definition and halting problem

Rowing machine definition and halting problem

System Fsub subtyping and typechecking problem

• Syntax of types and terms
• Subtyping and typechecking relations
• Subtyping and typechecking problems

System Fsub subtyping without arrow types

• Syntax of types
• Subtyping relation
• Subtyping problem

(Normal) System Fsub definition and subtyping problem

(Deterministic) System Fsub definition and subtyping problem

(Flattened) System Fsub definition and subtyping problem

Reductions

Reduction from Counter Machines to Rowing Machines

• Translation
• Reduction

Reduction from Counter Machines as defined in the Undecidability library to Counter Machines as defined by Pierce

• Translation
• Reduction

Reduction from Rowing Machines to Flattened System Fsub

• Translation
• Reduction

Reduction from Flattened System Fsub to Deterministic System Fsub

• Reduction

Reduction from the Deterministic System Fsub to the Normal System Fsub

• Translation
• Reduction

Reduction from the Normal System Fsub to the full System Fsub

• Reduction

Reduction from typechecking in the Normal System Fsub with arrows to typechecking in the full System Fsub with arrows

• Synthetic Reduction

Undecidability results

Undecidability of the halting problem of 2 Counter Machines a la Pierce

Undecidability of the halting problem of Rowing Machines

Undecidability of the subtyping problem of System FsubF

Undecidability of the subtyping problem of System FsubD

Undecidability of the subtyping and typechecking problems of System FsubN

Undecidability of the subtyping problem of System Fsub without arrow types

Undecidability of the subtyping and typechecking problems of System Fsub