Formal Certification of a Resource-Aware Language Implementation (Q3183530): Difference between revisions

@@ Property / author @@
-Ricardo Peña
@@ Property / author: Ricardo Peña / rank @@
-Normal rank
@@ Property / author @@
+Ricardo Peña
@@ Property / author: Ricardo Peña / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-03359-9_15
+Normal rank
@@ Property / OpenAlex ID @@
+W2105945150
@@ Property / OpenAlex ID: W2105945150 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4474214
@@ Property / cites work: Q4474214 / rank @@
+Normal rank
@@ Property / cites work @@
+Certificate Translation for Optimizing Compilers
@@ Property / cites work: Certificate Translation for Optimizing Compilers / rank @@
+Normal rank
@@ Property / cites work @@
+Static prediction of heap space usage for first-order functional programs
+Normal rank
@@ Property / cites work @@
+Verified bytecode verifiers.
@@ Property / cites work: Verified bytecode verifiers. / rank @@
+Normal rank
@@ Property / cites work @@
+Formal certification of a compiler back-end or
@@ Property / cites work: Formal certification of a compiler back-end or / rank @@
+Normal rank
@@ Property / cites work @@
+A formally verified compiler back-end
@@ Property / cites work: A formally verified compiler back-end / rank @@
+Normal rank
@@ Property / cites work @@
+Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
+Normal rank
@@ Property / cites work @@
+A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
+Normal rank
@@ Property / cites work @@
+An Inference Algorithm for Guaranteeing Safe Destruction
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q4809043
@@ Property / cites work: Q4809043 / rank @@
+Normal rank