Narcissus: correct-by-construction derivation of decoders and encoders from binary formats
It is a neat result from functional programming that libraries ofparser combinatorscan support rapid construc-tion of decoders for quite a range of formats. With a little more work, the same combinator program can denoteboth a decoder and an encoder. Unfortunately, the real world is full of gnarly f...
Main Authors: | Pit-Claudel, Clement Francois, Chlipala, Adam |
---|---|
Other Authors: | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
Format: | Article |
Language: | English |
Published: |
Association for Computing Machinery (ACM)
2021
|
Online Access: | https://hdl.handle.net/1721.1/130006 |
Similar Items
-
Compilation using correct-by-construction program synthesis
by: Pit-Claudel, Clément
Published: (2017) -
Narcissus.
by: Duong, Thi Dieu Linh., et al.
Published: (2012) -
The essence of Bluespec: a core language for rule-based hardware design
by: Bourgeat, Thomas, et al.
Published: (2021) -
Efficient encoding/decoding of irreducible words for codes correcting tandem duplications
by: Chee, Yeow Meng, et al.
Published: (2020) -
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
by: Pit-Claudel, Clement Francois, et al.
Published: (2021)