% Encoding: UTF-8

@InProceedings{FiatToFacade+IJCAR2020,
  author    = {Pit-Claudel, Clément and Wang, Peng and Delaware, Benjamin and Gross, Jason and Chlipala, Adam},
  title     = {Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs},
  booktitle = {Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II},
  year      = {2020},
  editor    = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
  volume    = {12167},
  series    = {Lecture Notes in Computer Science},
  pages     = {119-137},
  month     = jul,
  publisher = {Springer International Publishing},
  abstract  = {We present an original approach to sound program extraction in
               a proof assistant, using syntax-driven automation to derive
               correct-by-construction imperative programs from
               nondeterministic functional source code. Our approach does not
               require committing to a single inflexible compilation strategy
               and instead makes it straightforward to create domain-specific
               code translators. In addition to a small set of core
               definitions, our framework is a large, user-extensible
               collection of compilation rules each phrased to handle
               specific language constructs, code patterns, or data
               manipulations. By mixing and matching these pieces of logic,
               users can easily tailor extraction to their own domains and
               programs, getting maximum performance and ensuring correctness
               of the resulting assembly code.},
  doi       = {10.1007/978-3-030-51054-1_7},
  isbn      = {978-3-030-51054-1},
  url       = {https://pit-claudel.fr/clement/papers/fiat-to-facade-IJCAR20.pdf},
}