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...
Gardado en:
| Autor Principal: | |
|---|---|
| Formato: | Online |
| Idioma: | inglés |
| Publicado: |
KIT Scientific Publishing
2021
|
| Subjects: | |
| Acceso en liña: | 34320 |
| Tags: |
Sen Etiquetas, Sexa o primeiro en etiquetar este rexistro!
|
Títulos similares: Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
- 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
- A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
- Genre : didactique(s) et pratiques d'enseignement
- 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
- Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023
- Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings