Lazy Evaluation: From natural semantics to a machine-checked compiler transformation

• Auteur principal: Breitner, Joachim (auth)
• Format: Électronique Chapitre de livre
• Langue: anglais
• Publié: KIT Scientific Publishing 2016
• Sujets: Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle
• Accès en ligne: DOAB: download the publication; DOAB: description of the publication

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...