Dmitry Stefantsov 2aef206f3f [kernel] Add the first draft of Kernel operational semantics in Coq ...

The semantics is defined for a small subset of Kernel.

Change-Id: I39b72c5671e9ca0dee86a5a6068fe745ad1728f1
Reviewed-on: https://dart-review.googlesource.com/5860
Reviewed-by: Samir Jindel <sjindel@google.com>

2017-09-18 15:16:23 +00:00

..

Common.v

[kernel] Completion of consistency proofs for type system of first subset of kernel.

2017-09-18 11:37:03 +00:00

CommonTactics.v

[kernel] Completion of consistency proofs for type system of first subset of kernel.

2017-09-18 11:37:03 +00:00

ho-interpreter.sml

Add a reference interpreter in Standard ML

2017-09-15 10:42:44 +00:00

Makefile

[kernel] Completion of consistency proofs for type system of first subset of kernel.

2017-09-18 11:37:03 +00:00

ObjectModel.v

[kernel] Generalization of type equivalence to subtyping.

2017-09-18 11:47:31 +00:00

OperationalSemantics.v

[kernel] Add the first draft of Kernel operational semantics in Coq

2017-09-18 15:16:23 +00:00

Syntax.v

[kernel] Completion of consistency proofs for type system of first subset of kernel.

2017-09-18 11:37:03 +00:00

SyntaxRaw.v

[kernel] Proofs about type equality, beginnings of the type checking homomorphism proof.

2017-09-13 12:00:19 +00:00