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 Isabelle. To t...
Saved in:
| Main Author: | |
|---|---|
| Format: | Online |
| Language: | English |
| Published: |
KIT Scientific Publishing
2021
|
| Subjects: | |
| Online Access: | 34320 |
| Tags: |
No Tags, Be the first to tag this record!
|
Similar Items: Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
- Genre : didactique(s) et pratiques d'enseignement
- Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023
- Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022
- Fundamental Approaches to Software Engineering
- 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
- Kursbuch Informatik I. Formale Grundlagen der Informatik und Programmierkonzepte am Beispiel von Java. Eine Einführung in die Informatik auf der Grundlage etablierter Lehrbücher