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

@@ Property / author @@
-Andreas Lochbihler
@@ Property / author: Andreas Lochbihler / rank @@
-Normal rank
@@ Property / author @@
+Andreas Lochbihler
@@ Property / author: Andreas Lochbihler / 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 @@
+JavaFAN
@@ Property / describes a project that uses: JavaFAN / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CoqJVM
@@ Property / describes a project that uses: CoqJVM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+FinFuns
@@ Property / describes a project that uses: FinFuns / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Jinja Threads
@@ Property / describes a project that uses: Jinja Threads / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Tame Graphs
@@ Property / describes a project that uses: Tame Graphs / 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-22863-6_17
+Normal rank
@@ Property / OpenAlex ID @@
+W2106047869
@@ Property / OpenAlex ID: W2106047869 / rank @@
+Normal rank
@@ 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