PCF-redex

• An implementation of the Formal Semantics of the PCF Language, including Type-Inference Rules and Reduction Semantics.
• The majority of this code is inspired from OPLSS-2017 by Prof. David Van-Horn's lecture on Operational Semantics and Redex.
• I am working to extend the Semantics (Static and Dynamic) to add Higher-Order Contract Semantics and various other operators (both (Op) and a (Op) b)

Installation

• git clone git@github.com:jssandh2/pcf-redex.git
• Install DrRacket
• Run the file in DrRacket's REPL by clicking the Run button (afer Opening it).
• For instructions on how to play with the language, refer here : Redex Tutorial

Semantics

• The semantics correspond to that of PCF
• TODO :: Addition of Semantics and Reductions for :
  • (Op) and a (Op) b
  • is-zero and plus operators
  • Contract Semantics

Running PCF-redex

• TODO :: Implementation of the helper functions ext and lookup
• Coming Soon!