Project Page Index Table of Contents
  • Preliminaries
  • Definition of L
    • Syntax
    • Named abstractions
    • Substitution and closedness
    • Named procedures
    • Evaluation relation
  • Uniformly confluent reduction semantics
    • One-step reduction
    • Reflexive-transitive closure and step-indexed closure
    • Recursion operator
    • Reduction equivalence
  • Automation for equivalences and reductions
    • Tactics for closedness and abstractions
    • Tactics to solve equivalences and reductions
  • Scott encoding of numbers
  • Scott encoding of terms
    • Scott encoding of booleans
  • Decidable and recognisable classes
    • Definition of decidable classes
    • Definition of recognisable classes
    • Decidable classes are closed under union, intersection and complement
    • There is an undecidable class
    • Recognisable classes are closed under intersection
    • Decidable classes are recognisable and coregnisable
    • Scott's theorem
  • Reduction lemma and Rice’s theorem
    • Closedness is decidable
    • Reduction lemma
    • Rice's lemma and Rice's theorem
  • Step-indexed interpreter and modesty
    • Step-indexed interpreter
    • Modesty
  • Results obtained with self-interpreters
    • Step-indexed self-interpreter
      • Encoding of options
      • Equality of encoded natural numbers
      • Substitution
      • Step-indexed self-interpreter
    • Class of total procedures is unrecognisable
    • Self-interpreter
    • Parallel or
    • Post's theorem
    • Recognisable classes are closed under union
  • Enumerable classes
    • Definition of enumerable classes
    • Enumerable classes are recognisable
      • Equality of encoded terms
      • Search using Choose
    • Terms are countable
  • Countable Types
    • Procedural realisation of enumeration
    • Some list procedures
    • Recognisable classes are enumerable
  • Markov's principle
  • Reducability
  • Additional results not mentioned in the paper
    • Natural numbers
      • Predecessor and multiplication
    • Trivial and finite classes are decidable
    • First fixed-point theorem
    • Some corollaries of Rice's theorem
  • Lines of code for major results
Generated by coqdoc and improved with CoqdocJS