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

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

Name		Name	Last commit message	Last commit date
Latest commit History 16 Commits
.gitignore		.gitignore
LICENSE		LICENSE
Leture-2-Dependent-Types.rkt		Leture-2-Dependent-Types.rkt
README.md		README.md
ba.rkt		ba.rkt
pcf-tests.rkt		pcf-tests.rkt
pcf.rkt		pcf.rkt
tba.rkt		tba.rkt