Andere Kunden interessierten sich auch für
![A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler]( "A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler")
A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler41,00 €![From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security]( "From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security")
From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security37,00 €![Model Transformation Languages with Modular Information Hiding]( "Model Transformation Languages with Modular Information Hiding")
Model Transformation Languages with Modular Information Hiding48,00 €![Programming in Prolog]( "Programming in Prolog")
Programming in Prolog57,99 €![Compilers]( "Compilers")
Compilers73,99 €![Complete Guide to Test Automation]( "Complete Guide to Test Automation")
Complete Guide to Test Automation43,99 €![Intelligent Speculative Compiler Optimizations]( "Intelligent Speculative Compiler Optimizations")
Intelligent Speculative Compiler Optimizations89,90 €
In order to solve a long-standing problem with list fusion, a new compiler transformation, "Call Arity" is developed and implemented in the Haskell compiler GHC. It is formally proven to not degrade program performance; the proof is machine-checked using the interactive theorem prover Isabelle. To that end, a formalization of Launchbury's Natural Semantics for Lazy Evaluation is modelled in Isabelle, including a correctness and adequacy proof.