References

  1. Jean-Raymond Abrial (1996): The B-Book: Assigning Programs to Meanings. Cambridge University Press, doi:10.1017/CBO9780511624162.
  2. Denis Bogdănaş & Grigore Roşu (2015): K-Java: A Complete Semantics of Java. In: Proc. 42nd ACM Symposium on Principles of Programming Languages (POPL), pp. 445–456, doi:10.1145/2676726.2676982.
  3. Darren Cofer, Isaac Amundson, Ramachandra Sattigeri, Arjun Passi, Christopher Boggs, Eric Smith, Limei Gilham, Taejoon Byun & Sanjai Rayadurgam (2020): Run-Time Assurance for Learning-Based Aircraft Taxiing. In: Proc. 39th Digital Avionics Systems Conference (DASC), doi:10.1109/DASC50938.2020.9256581.
  4. Alessandro Coglio (2018): A Formalization of the ABNF Notation and a Verified Parser of ABNF Grammars. In: Proc. 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), Lecture Notes in Computer Science (LNCS) 11294, pp. 177–195, doi:10.1007/978-3-030-03592-1_10.
  5. 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.
  6. Alessandro Coglio (2022): A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2. In: Proc. 17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022).
  7. 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), Electronic Proceedings in Theoretical Computer Science (EPTCS) 259, pp. 61–77, doi:10.4204/EPTCS.249.5.
  8. 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.
  9. Coq 8.15.0 Reference Manual. https://coq.inria.fr.
  10. Florian Haftmann with contributions from Lukas Bulwahn (2021): Code generation from Isabelle/HOL theories. https://isabelle.in.tum.de. Tutorial distributed with Isabelle/HOL.
  11. Cliff Jones (1990): Systematic Software Development using VDM, second edition. Prentice Hall.
  12. Neil D. Jones, Carsten K. Gomard & Peter Sestoft (1999): Partial Evaluation and Automatic Program Generation. Prentice Hall. http://www.itu.dk/people/sestoft/pebook.
  13. Kestrel Institute: APT. https://www.kestrel.edu/research/apt.
  14. Kestrel Institute: Specware. https://www.kestrel.edu/research/specware.
  15. Tobias Nipkow & David von Oheimb (1998): Java Light is Type-Safe — Definitely. In: Proc. 25th ACM Symposium on Principles of Programming Languages (POPL), pp. 161–170, doi:10.1145/268946.268960.
  16. Nararajan Shankar (2017): A Brief Introduction to the PVS2C Code Generator. In: Proc. Workshop on Automated Formal Methods (AFM'17).
  17. J. M. Spivey (1992): The Z Notation: A Reference Manual, second edition. Prentice Hall.
  18. Robert Stärk, Joachim Schmid & Egon Börger (2001): Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, doi:10.1007/978-3-642-59495-3.
  19. The ACL2 Community: The ACL2 Theorem Prover and Community Books: Documentation. http://acl2.org/manual.
  20. The ACL2 Community: The ACL2 Theorem Prover and Community Books: Source Code. http://github.com/acl2/acl2.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org