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 [email protected]: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!