Dmitry Stefantsov 172aecaac8 [kernel-f11n] Move another helper theorem about maps to Common.v ...

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

2017-10-02 15:15:40 +00:00

..

_CoqProject

[kernel-coq] Extend interfaces to contain getters.

2017-09-26 17:39:15 +00:00

build.sh

[kernel-coq] Cleaning up and exposing program well-formedness proof.

2017-09-22 11:55:53 +00:00

Common.v

[kernel-f11n] Move another helper theorem about maps to Common.v

2017-10-02 15:15:40 +00:00

CommonTactics.v

[kernel-f11n] Cleanup to object model.

2017-09-28 14:20:01 +00:00

ho-interpreter.sml

Add a reference interpreter in Standard ML

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

ObjectModel.v

[kernel-f11n] Cleanup to object model.

2017-09-28 14:20:01 +00:00

OperationalSemantics.v

[kernel-f11n] Fix operational semantics w.r.t. changes in object model

2017-09-29 08:15:03 +00:00

OperationalSemanticsProof.v

[kernel-f11n] Move another helper theorem about maps to Common.v

2017-10-02 15:15:40 +00:00

Syntax.v

[kernel-f11n] Fix statement typing and complete proof of statement typing consistency.

2017-09-28 13:20:00 +00:00

SyntaxRaw.v

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

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