Cogent: uniqueness types and certifying compilation. (27th October 2021)
- Record Type:
- Journal Article
- Title:
- Cogent: uniqueness types and certifying compilation. (27th October 2021)
- Main Title:
- Cogent: uniqueness types and certifying compilation
- Authors:
- O'CONNOR, LIAM
CHEN, ZILIN
RIZKALLAH, CHRISTINE
JACKSON, VINCENT
AMANI, SIDNEY
KLEIN, GERWIN
MURRAY, TOBY
SEWELL, THOMAS
KELLER, GABRIELE - Abstract:
- Abstract: This paper presents a framework aimed at significantly reducing the cost of proving functional correctness for low-level operating systems components. The framework is designed around a new functional programming language, Cogent. A central aspect of the language is its uniqueness type system, which eliminates the need for a trusted runtime or garbage collector while still guaranteeing memory safety, a crucial property for safety and security. Moreover, it allows us to assign two semantics to the language: The first semantics is imperative, suitable for efficient C code generation, and the second is purely functional, providing a user-friendly interface for equational reasoning and verification of higher-level correctness properties. The refinement theorem connecting the two semantics allows the compiler to produce a proof via translation validation certifying the correctness of the generated C code with respect to the semantics of the Cogent source program. We have demonstrated the effectiveness of our framework for implementation and for verification through two file system implementations.
- Is Part Of:
- Journal of functional programming. Volume 31(2021)
- Journal:
- Journal of functional programming
- Issue:
- Volume 31(2021)
- Issue Display:
- Volume 31, Issue 2021 (2021)
- Year:
- 2021
- Volume:
- 31
- Issue:
- 2021
- Issue Sort Value:
- 2021-0031-2021-0000
- Page Start:
- Page End:
- Publication Date:
- 2021-10-27
- Subjects:
- Functional programming (Computer science) -- Periodicals
- Journal URLs:
- http://journals.cambridge.org/action/displayJournal?jid=JFP ↗
http://firstsearch.oclc.org ↗ - DOI:
- 10.1017/S095679682100023X ↗
- Languages:
- English
- ISSNs:
- 0956-7968
- Deposit Type:
- Legaldeposit
- View Content:
- Available online (eLD content is only available in our Reading Rooms) ↗
- Physical Locations:
- British Library STI - ELD Digital store
- Ingest File:
- 19696.xml