The end of history? Using a proof assistant to replace language design with library design

Functionality of software systems has exploded in part because of advances in programming language support for packaging reusable functionality as libraries. Developers benefit from the uniformity that comes of exposing many interfaces in the same language, as opposed to stringing together hodgepodg...

Full description

Bibliographic Details
Main Authors: Chlipala, Adam, Delaware, Benjamin, Duchovni, Samuel, Gross, Jason S., Pit-Claudel, Clément, Suriyakarn, Sorawit, Wang, Peng
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory
Format: Article
Language:English
Published: Dagstuhl Research 2021
Online Access:https://hdl.handle.net/1721.1/128880.2