Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
Topics & Concepts
Computer scienceProgramming languageCorrectnessMathematical proofSet (abstract data type)Assembly languageCode (set theory)Theoretical computer scienceSoftwareGeometryMathematicsLogic, programming, and type systemsSoftware Engineering ResearchSecurity and Verification in Computing