Animating the Formalised Semantics of a Java-Like Language (Q3088008): Difference between revisions

@@ Property / cites work @@
+CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
+Normal rank
@@ Property / cites work @@
+Interpretation of Locales in Isabelle: Theories and Proof Contexts
+Normal rank
@@ Property / cites work @@
+Turning Inductive into Equational Specifications
@@ Property / cites work: Turning Inductive into Equational Specifications / rank @@
+Normal rank
@@ Property / cites work @@
+Imperative Functional Programming with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Algebraic Methodology and Software Technology
@@ Property / cites work: Algebraic Methodology and Software Technology / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+The Isabelle Collections Framework
@@ Property / cites work: The Isabelle Collections Framework / 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 @@
+Extraction in Coq: An Overview
@@ Property / cites work: Extraction in Coq: An Overview / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying a Compiler for Java Threads
@@ Property / cites work: Verifying a Compiler for Java Threads / rank @@
+Normal rank
@@ Property / cites work @@
+Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Certification of Termination Proofs Using CeTA
@@ Property / cites work: Certification of Termination Proofs Using CeTA / rank @@
+Normal rank