Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
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 Isab...
Saved in:
Main Author: | Breitner, Joachim (auth) |
---|---|
Format: | Electronic Book Chapter |
Language: | English |
Published: |
KIT Scientific Publishing
2016
|
Subjects: | |
Online Access: | DOAB: download the publication DOAB: description of the publication |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Similar Items
-
A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
by: Lochbihler, Andreas
Published: (2012) -
Bridging Formal and Conceptual Semantics Selected papers of BRIDGE-14
Published: (2017) -
Fundamental Approaches to Software Engineering: 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings
by: Alessandra Russo
Published: (2018) -
Fundamental Approaches to Software Engineering 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings
Published: (2018) -
Fundamental Approaches to Software Engineering 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings
Published: (2018)