2 papers
cs.PL2018
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu +10
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to dischar…
cs.PL2018
Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit--Claudel +2
It is a neat result from functional programming that libraries of parser combinators can support rapid construction of decoders for quite a range of formats. With a little more wor…