Fiat

DOI10.1145/2676726.2677006zbMath1346.68175OpenAlexW1976978933MaRDI QIDQ2819861

Jason Gross, Clément Pit-Claudel, Adam Chlipala, Benjamin Delaware

Publication date: 29 September 2016

Published in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2676726.2677006

zbMATH Keywords

deductive synthesismechanized derivation of abstract data types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers, Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs, Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques, Foundations of dependent interoperability, Automatic refinement to efficient data structures: a comparison of two approaches, Bootstrapping library-based synthesis, Verified Characteristic Formulae for CakeML, Refinement to imperative HOL, From Sets to Bits in Coq, Extensible and Efficient Automation Through Reflective Tactics, Constructive Galois Connections, Fiat

Uses Software

• Coq
• OCaml
• KIDS
• DTRE