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

 0 Người đánh giá. Xếp hạng trung bình 0

Tác giả: Joachim Breitner

Ngôn ngữ: eng

ISBN-13: 978-3731505464

ISBN: KSP/1000056002

Ký hiệu phân loại: 004 Data processing || Computer science

Thông tin xuất bản: Karlsruhe : KIT Scientific Publishing, 2016

Mô tả vật lý: 1 electronic resource (XIV, 231 p. p.)

Bộ sưu tập: Tài liệu truy cập mở

ID: 233383

 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 that end, a formalization of Launchbury's Natural Semantics for Lazy Evaluation is modelled in Isabelle, including a correctness and adequacy proof.
Tạo bộ sưu tập với mã QR

THƯ VIỆN - TRƯỜNG ĐẠI HỌC CÔNG NGHỆ TP.HCM

ĐT: (028) 71010608 | Email: tt.thuvien@hutech.edu.vn

Copyright @2024 THƯ VIỆN HUTECH