Skip to main content
SpringerLink
Log in

The Proof Assistant as an Integrated Development Environment

  • Conference paper
Programming Languages and Systems (APLAS 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8301))

Included in the following conference series:

Abstract

We discuss the potential of doing program development, code generation, application-specific modelling, and verification entirely within a proof assistant.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. CUP (2014)

    Google Scholar 

  2. Benton, N., Kennedy, A., Varming, C.: Some domain theory and denotational semantics in Coq. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 115–130. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: TCP, UDP, and Sockets: Rigorous and experimentally-validated behavioural specification. volume 2: The specification. Technical Report 625, University of Cambridge Computer Laboratory (2005)

    Google Scholar 

  4. Braibant, T., Pous, D.: An efficient Coq tactic for deciding Kleene algebras. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 163–178. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Chlipala, A.: The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In: ACM International Conference on Functional Programming, ICFP (2013)

    Google Scholar 

  6. Conway, M.E.: Proposal for an UNCOL. Communications of the ACM 1(10), 5–8 (1958)

    Article  MATH  Google Scholar 

  7. Jensen, J., Benton, N., Kennedy, A.: High-level separation logic for low-level code. In: ACM Symposium on Principles of Programming Languages, POPL (2013)

    Google Scholar 

  8. Kennedy, A., Benton, N., Jensen, J., Dagand, P.: Coq: The world’s best macro assembler? In: International Symposium on Principles and Practice of Declarative Programming, PPDP (2013)

    Google Scholar 

  9. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: Sel4: Formal verification of an OS kernel. In: 22nd ACM Symposium on Operating Systems Principles, SOSP (2009)

    Google Scholar 

  10. Koprowski, A., Binsztok, H.: TRX: A formally verified parser interpreter. Logical Methods in Computer Science 7(2) (2011)

    Google Scholar 

  11. Kumar, R., Myreen, M.O., Owens, S.A., Norrish, M.: CakeML: A verified implementation of ML. In: ACM Symposium on Principles of Programming Languages, POPL (2014)

    Google Scholar 

  12. Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  13. Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: ACM Symposium on Principles of Programming Languages, POPL (2010)

    Google Scholar 

  14. Myreen, M.O.: Verified just-in-time compiler on x86. In: ACM Symposium on Principles of Programming Languages, POPL (2010)

    Google Scholar 

  15. Myreen, M.O., Gordon, M.J.C.: Function extraction. Science of Computer Programming (2010)

    Google Scholar 

  16. Myreen, M.O., Slind, K., Gordon, M.J.C.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: Formal Methods in Computer-Aided Design, FMCAD (2008)

    Google Scholar 

  17. Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Reasoning with the awkward squad. In: ACM International Conference on Functional Programming, ICFP (2008)

    Google Scholar 

  18. Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: ACM Symposium on Principles of Programming Languages, POPL (2006)

    Google Scholar 

  19. Sarkar, S., Sewell, P., Zappa Nardelli, F., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-cc multiprocessor machine code. In: ACM Symposium on Principles of Programming Languages, POPL (2009)

    Google Scholar 

  20. Strub, P.-Y., Swamy, N., Fournet, C., Chen, J.: Self-certification: Bootstrapping certified typecheckers in F* with Coq. In: ACM Symposium on Principles of Programming Languages, POPL (2012)

    Google Scholar 

  21. Wisnesky, R., Malecha, G., Morrisett, G.: Certified web services in Ynot. In: International Workshop on Automated Specification and Verification of Web Systems, WWV (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, UK

    Nick Benton

Authors
  1. Nick Benton
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Indiana University, 150 S. Woodlawn Avenue, 47405-7104, Bloomington, IN, USA

    Chung-chieh Shan

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer International Publishing Switzerland

About this paper

Cite this paper

Benton, N. (2013). The Proof Assistant as an Integrated Development Environment. In: Shan, Cc. (eds) Programming Languages and Systems. APLAS 2013. Lecture Notes in Computer Science, vol 8301. Springer, Cham. https://doi.org/10.1007/978-3-319-03542-0_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-03542-0_22

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-03541-3

  • Online ISBN: 978-3-319-03542-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation