A Sound Semantics for OCaml light
From MaRDI portal
Recommendations
- Towards Self-verification of HOL Light
- HOL with definitions: semantics, soundness, and a verified implementation
- scientific article; zbMATH DE number 1670740
- Mechanized semantics for the clight subset of the C language
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
Cited in
(18)- Winskel is (almost) right: Towards a mechanized semantics textbook
- Mechanized semantics for the clight subset of the C language
- scientific article; zbMATH DE number 1670740 (Why is no real title available?)
- Automating soundness proofs
- Lem: reusable engineering of real-world semantics
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- HOL with definitions: semantics, soundness, and a verified implementation
- Lem: a lightweight tool for heavyweight semantics
- Towards a mechanized metatheory of Standard ML
- A Brief Overview of HOL4
- Towards Self-verification of HOL Light
- scientific article; zbMATH DE number 2090729 (Why is no real title available?)
- Ott, effective tool support for the working semanticist
- A certified implementation of ML with structural polymorphism and recursive types
- Importing HOL Light into Coq
- Structural operational semantics through context-dependent behaviour
- Winskel is (almost) right. Towards a mechanized semantics textbook
- An operational semantics for object-oriented concepts based on the class hierarchy
This page was built for publication: A Sound Semantics for OCaml light
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458382)
