References

  1. Jean-Raymond Abrial (1996): The B-Book: Assigning Programs to Meanings. Cambridge University Press, doi:10.1017/CBO9780511624162.
  2. Alessandro Coglio (2014): Pop-Refinement. Archive of Formal Proofs. http://afp.sf.net/entries/Pop_Refinement.shtml, Formal proof development.
  3. Alessandro Coglio (2018): A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java. In: Proc. 15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2018), Electronic Proceedings in Theoretical Computer Science (EPTCS) 280, pp. 1–17, doi:10.4204/EPTCS.280.1.
  4. Alessandro Coglio (2022): A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java. In: Proc. 17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022).
  5. Alessandro Coglio, Matt Kaufmann & Eric Smith (2017): A Versatile, Sound Tool for Simplifying Definitions. In: Proc. 14th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2017), pp. 61–77, doi:10.4204/EPTCS.249.5.
  6. Alessandro Coglio & Stephen Westfold (2020): Isomorphic Data Type Transformations. In: Proc. 16th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2020), Electronic Proceedings in Theoretical Computer Science (EPTCS) 327, pp. 125–141, doi:10.4204/EPTCS.280.1.
  7. Coq 8.15.0 Reference Manual. https://coq.inria.fr.
  8. Chucky Ellison & Grigore Rosu (2012): An Executable Formal Semantics of C with Applications. In: Proc. 39th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 533–544, doi:10.1145/2103656.2103719.
  9. Florian Haftmann with contributions from Lukas Bulwahn (2021): Code generation from Isabelle/HOL theories. https://isabelle.in.tum.de. Tutorial distributed with Isabelle/HOL.
  10. Yuri Gurevich & James K. Huggins (1992): The Semantics of the C Programming Language. In: Proc. 6th International Workshop on Computer Science Logic (CSL), Lecture Notes in Computer Science (LNCS) 702, pp. 274–308, doi:10.1007/3-540-56992-8_17.
  11. ISO/IEC (2018): ISO/IEC 9899: Information Technology — Programming Languages — C. International Standard. Fourth Edition.
  12. Cliff Jones (1990): Systematic Software Development using VDM, second edition. Prentice Hall.
  13. Neil D. Jones, Carsten K. Gomard & Peter Sestoft (1999): Partial Evaluation and Automatic Program Generation. Prentice Hall. http://www.itu.dk/people/sestoft/pebook.
  14. Kestrel Institute: APT (Automated Program Transformations). https://www.kestrel.edu/research/apt.
  15. Kestrel Institute: Specware. https://www.kestrel.edu/research/specware.
  16. Xavier Leroy (2009): Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning (JAR) 43(3), pp. 263–288, doi:10.1007/s10817-009-9148-3.
  17. Michael Norrish (1998): C formalised in HOL. University of Cambridge.
  18. Nikolaos S. Papaspyrou (1998): A Formal Semantics for the C Programming Language. National Technical University of Athens.
  19. David M. Russinoff (2022): Formal Verification of Floating-Point Hardware Design, 2nd edition. Springer, doi:10.1007/978-3-030-87181-9.
  20. Nararajan Shankar (2017): A Brief Introduction to the PVS2C Code Generator. In: Proc. Workshop on Automated Formal Methods (AFM'17).
  21. J. M. Spivey (1992): The Z Notation: A Reference Manual, second edition. Prentice Hall.
  22. The ACL2 Community: The ACL2 Theorem Prover and Community Books: Documentation. http://acl2.org/manual.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org