2 options
Don't mind the formalization gap : the design and usage of hs-to-coq / Antal Spector-Zabusky.
- Format:
- Book
- Thesis/Dissertation
- Author/Creator:
- Spector-Zabusky, Antal, author.
- Language:
- English
- Subjects (All):
- Computer science.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Local Subjects:
- Computer science.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Genre:
- Academic theses.
- Physical Description:
- 1 online resource (241 pages)
- Contained In:
- Dissertations Abstracts International 82-12B.
- Other Title:
- Do not mind the formalization gap
- Place of Publication:
- [Philadelphia, Pennsylvania] : University of Pennsylvania ; Ann Arbor : ProQuest Dissertations & Theses, 2021.
- Language Note:
- English
- System Details:
- Mode of access: World Wide Web.
- text file
- Summary:
- Using proof assistants to perform formal, mechanical software verification is a powerful technique for producing correct software. However, the verification is time-consuming and limited to software written in the language of the proof assistant. As an approach to mitigating this tradeoff, this dissertation presents hs-to-coq, a tool for translating programs written in the Haskell programming language into the Coq proof assistant, along with its applications and a general methodology for using it to verify programs. By introducing edit files containing programmatic descriptions of code transformations, we provide the ability to flexibly adapt our verification goals to exist anywhere on the spectrum between "increased confidence" and "full functional correctness".
- Notes:
- Source: Dissertations Abstracts International, Volume: 82-12, Section: B.
- Advisors: Weirich, Stephanie; Committee members: Steve Zdancewic; Benjamin Pierce; Mayur Naik; Andrew Appel.
- Department: Computer and Information Science.
- Ph.D. University of Pennsylvania 2021.
- Local Notes:
- School code: 0175
- ISBN:
- 9798738648472
- Access Restriction:
- Restricted for use by site license.
- This item must not be sold to any third party vendors.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.