Investigating type-certifying compilation with Isabelle
From MaRDI portal
Recommendations
- An expressive, scalable type theory for certified code
- scientific article; zbMATH DE number 2086518
- Language-based program verification via expressive types
- Efficient Verified Programs in a Type Theory with Mixed Constructivity
- Verification of non-functional programs using interpretations in type theory
- Program and proof optimizations with type systems
- scientific article; zbMATH DE number 6296049
- scientific article; zbMATH DE number 3928328
Cited in
(13)- Mechanising a type-safe model of multithreaded Java with a verified compiler
- Verified bytecode verification and type-certifying compilation
- A self-certifying compilation framework for WebAssembly
- Java: Embedding a programming language in a theorem prover
- Formal Certification of a Resource-Aware Language Implementation
- Certifying supercompilation for Martin-Löf's type theory
- Scalable certification for typed assembly language
- scientific article; zbMATH DE number 2165694 (Why is no real title available?)
- scientific article; zbMATH DE number 2090288 (Why is no real title available?)
- Cogent: uniqueness types and certifying compilation
- Certifying dictionary construction in Isabelle/HOL
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Certifying compilers using higher-order theorem provers as certificate checkers
This page was built for publication: Investigating type-certifying compilation with Isabelle
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4428314)
