Skip to content

Latest commit

 

History

History
60 lines (32 loc) · 2.06 KB

README.md

File metadata and controls

60 lines (32 loc) · 2.06 KB

KappaF

This repository contains the Coq sources for the formalisation of KappaF and the proof of its type soundness. There is a Makefile for compiling the scripts (cleaning the produced files). It also has a rule "make count" to show the number of lines for definitions and properties/proofs respectively. The source files are the following:

Definitions

  • Meta.v - Definitions of identifiers and partial maps

  • Syntax.v - The syntax of KappaF

  • Dynamic.v - The dynamic semantics of KappaF

  • Types.v - The static semantics of KappaF

  • WellFormedness.v - The definitions of well-formed configurations

Properties and proofs

  • [MetaProp - Properties](KappaF/MetaProp - Properties) of identifiers and maps, and their proofs

  • [SyntaxProp - Properties](KappaF/SyntaxProp - Properties) of the syntax their proofs

  • [DynamicProp - Properties](KappaF/DynamicProp - Properties) of the dynamic semantics the their proofs

  • [TypesProp - Properties](KappaF/TypesProp - Properties) of the static semantics and their proofs

  • [WellFormednessProp - Properties](KappaF/WellFormednessProp - Properties) of well-formedness rules and their proofs

  • Locking.v - Lemmas and theorems about locking

  • Progress.v - The proof of progress

  • Preservation.v - The proof of preservation

  • Soundness.v - The proof of type soundness

Miscellaneous

Libraries

License

This source code is released under the CRAPL license.