Project Page
Index
Table of Contents
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