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

• Yazar: Breitner, Joachim (auth)
• Materyal Türü: Elektronik Kitap Bölümü
• Dil: İngilizce
• Baskı/Yayın Bilgisi: KIT Scientific Publishing 2016
• Konular: Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle
• Online Erişim: 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...