Library syntax
Syntactic elements
Library model_structure
A carrier structure for the models
Library model_validity_cbv
Additional structure for call-by-value models
Library model_validity_cbn
Additional structure for call-by-name models
Library model_validity_generic
Generic constructions for the models, regardless of CBV/CBN
Library nbe_cbv_atomic
Call-by-VALUE TDPE for shift and reset, restriction to an atomic
Evaluator of typed terms in Kripke models (aka Soundness)
The reifyer from Kripke models to terms in normal form (aka Completeness for the Universal model)
Now we can define NbE as composition of soundness and completeness
Library nbe_cbn_atomic
Call-by-NAME TDPE for shift and reset, restriction to an atomic
Evaluator of typed terms in Kripke models (aka Soundness)
The reifyer from Kripke models to terms in normal form (aka Completeness for the Universal model)
Now we can define NbE as composition of soundness and completeness
Library nbe_tests
This page has been generated by
coqdoc