Project Page Index Table of Contents

Real.LPar
  • Propositional Logic
    • Types
    • Contexts
    • Typing judgments
  • Realizability
    • Generic realizability structure
  • Realizability interpretations
    • Version (1)
    • Version (2)

Real.MuMutilde
  • Propositional Logic
    • Types
    • Contexts
    • Typing judgments
  • Realizability
    • Generic realizability structure
  • Realizability interpretations
    • Version (1): call-by-name
    • Version (2): Call-by-value arrow type, call-by-name product type
    • Version (3): Call-by-name arrow type, call-by-value product type
    • Version (4): Call-by-value
    • Version (2bis)
    • Version (1bis)
    • Version (4bis)
Generated by coqdoc and improved with CoqdocJS