Function extraction (Q436372): Difference between revisions

@@ Property / cites work @@
+Transforming Programs into Recursive Functions
@@ Property / cites work: Transforming Programs into Recursive Functions / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+An axiomatic basis for computer programming
@@ Property / cites work: An axiomatic basis for computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+Partial functions in ACL2
@@ Property / cites work: Partial functions in ACL2 / 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 @@
+Verified just-in-time compiler on x86
@@ Property / cites work: Verified just-in-time compiler on x86 / rank @@
+Normal rank
@@ Property / cites work @@
+Verification of non-functional programs using interpretations in type theory
+Normal rank
@@ Property / cites work @@
+Q2763683
@@ Property / cites work: Q2763683 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Theorems about LISP Functions
@@ Property / cites work: Proving Theorems about LISP Functions / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Automated proofs of object code for a widely used microprocessor
+Normal rank
@@ Property / cites work @@
+Certified assembly programming with embedded code pointers
+Normal rank
@@ Property / cites work @@
+Using XCAP to Certify Realistic Systems Code: Machine Context Management
+Normal rank
@@ Property / cites work @@
+Stack-based typed assembly language
@@ Property / cites work: Stack-based typed assembly language / rank @@
+Normal rank
@@ Property / cites work @@
+Avoiding exponential explosion
@@ Property / cites work: Avoiding exponential explosion / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient weakest preconditions
@@ Property / cites work: Efficient weakest preconditions / rank @@
+Normal rank
@@ Property / cites work @@
+Verification Condition Generation Via Theorem Proving
+Normal rank
@@ Property / cites work @@
+Q5674963
@@ Property / cites work: Q5674963 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5633670
@@ Property / cites work: Q5633670 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Science Logic
@@ Property / cites work: Computer Science Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Types, bytes, and separation logic
@@ Property / cites work: Types, bytes, and separation logic / rank @@
+Normal rank
@@ Property / cites work @@
+A Formalisation of Smallfoot in HOL
@@ Property / cites work: A Formalisation of Smallfoot in HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Q4738240
@@ Property / cites work: Q4738240 / rank @@
+Normal rank