Project Page Index Table of Contents

RSC.Decidable

RSC.lib
    • Context Lookup
    • everything below has to be reviewed

RSC.ARS
  • Abstract Reduction Systems

RSC.vrel
  • Correspondence Relations on variables / de Bruijn indices
    • Map and Append
    • Extension of Var Relations
    • Functionality
    • Injectivity
    • Range-Disjointedness
    • The Identity Var Relations

RSC.pts
  • Church Rosser for Pure Type Systems
    • Genralised Pure Type System
    • Parametrisation
    • Syntax
    • Normal Terms
    • Reduction
    • Reduction and Instantiation
    • Confluence and Church Rosser
    • Free Variables
    • Typing
    • Validity of contexts
    • Strengthening

RSC.stlc
  • Traditional, 2-sorted STLC with one abstract base type, derived from 2-sorted SysF of the CPP paper
    • Syntax
    • Type System
    • Theory
    • Propagation
    • Validity of Contexts
    • Internalising contexts

RSC.stlcCorrespondence
  • Correspondence Result for STLC
    • Internalising contexts
    • REMARK:
    • Correspondence
    • Relating Types
    • Relating terms
    • Valid Contexts always have related Counterparts
    • Correspondence for Closed Judgements
    • Demos

RSC.sysf
  • Traditional, 2-sorted System F with explicits type variable contexts, a la Harper
    • Syntax
    • Type System
    • Theory
    • Validity of contexts
    • Internalising valid contexts, staged: first terms then types

RSC.sysfCorrespondence
  • Correspondence Result for System F
    • Internalising contexts
    • Correspondence
    • Relating Types
    • Relating terms
    • Valid Contexts always have related Counterparts
    • Correspondence for Closed Judgements
    • Demos
Generated by coqdoc and improved with CoqdocJS