Skip to main content
SpringerLink
Log in

Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types

  • Conference paper
Interactive Theorem Proving (ITP 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7998))

Included in the following conference series:

Abstract

This paper extends the proof methods used by the Nuprl proof assistant to reason about the computational behavior of its untyped programs. We have implemented new methods to prove non-trivial bisimulations between programs and have successfully applied these methods to formally optimize distributed programs such as our synthesized and verified version of Paxos, a widely used protocol to achieve software based replication. We prove new results about the basic computational equality relation on terms, and we extend the theory of partial types as the basis for stating internal results about the computation system that were previously treated only in the meta theory of Nuprl. All the lemmas presented in this paper have been formally proved in Nuprl.

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. The Coq Proof Assistant, http://coq.inria.fr/

  2. Allen, S.F.: A non-type-theoretic definition of martin-löf’s types. In: LICS, pp. 215–221. IEEE Computer Society (1987)

    Google Scholar 

  3. Allen, S.F.: A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University (1987)

    Google Scholar 

  4. Allen, S.F., Bickford, M., Constable, R.L., Eaton, R., Kreitz, C., Lorigo, L., Moran, E.: Innovations in computational type theory using Nuprl. J. Applied Logic 4(4), 428–469 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  5. Aspinall, D., Beringer, L., Momigliano, A.: Optimisation validation. Electr. Notes Theor. Comput. Sci. 176(3), 37–59 (2007)

    Article  MathSciNet  Google Scholar 

  6. Barzilay, E.: Implementing Reflection in Nuprl. PhD thesis, Cornell University (2006)

    Google Scholar 

  7. Berghofer, S.: Program extraction in simply-typed higher order logic. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 21–38. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 24–40. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer (2004)

    Google Scholar 

  10. Bickford, M.: Component specification using event classes. In: Lewis, G.A., Poernomo, I., Hofmeister, C. (eds.) CBSE 2009. LNCS, vol. 5582, pp. 140–155. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  11. Bickford, M., Constable, R., Guaspari, D.: Generating event logics with higher-order processes as realizers. Technical report, Cornell University (2010)

    Google Scholar 

  12. Bickford, M., Constable, R.L.: Formal foundations of computer security. In: NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 14, pp. 29–52 (2008)

    Google Scholar 

  13. Bickford, M., Constable, R.L., Rahli, V.: Logic of events, a framework to reason about distributed systems. In: Languages for Distributed Algorithms Workshop (2012)

    Google Scholar 

  14. Charron-Bost, B., Schiper, A.: The Heard-Of model: Computing in distributed systems with benign failures. Distributed Computing 22(1), 49–71 (2009)

    Article  MATH  Google Scholar 

  15. Chlipala, A.: A verified compiler for an impure functional language. In: 37th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 93–106. ACM (2010)

    Google Scholar 

  16. Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., Upper Saddle River (1986)

    Google Scholar 

  17. Constable, R.L., Smith, S.F.: Computational foundations of basic recursive function theory. Theoretical Computer Science 121(1&2), 89–112 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  18. Crary, K.: Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Cornell University, Ithaca, NY (August 1998)

    Google Scholar 

  19. Dave, M.A.: Compiler verification: a bibliography. ACM SIGSOFT Software Engineering Notes 28(6), 2 (2003)

    Article  Google Scholar 

  20. Gordon, A.D.: Bisimilarity as a theory of functional programming. Electr. Notes Theor. Comput. Sci. 1, 232–252 (1995)

    Article  Google Scholar 

  21. Hickey, J., et al.: MetaPRL - A modular logical environment. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 287–303. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  22. Hickey, J.J.: The MetaPRL Logical Programming Environment. PhD thesis, Cornell University, Ithaca, NY (January 2001)

    Google Scholar 

  23. Howe, D.J.: Equality in lazy computation systems. In: Proceedings of Fourth IEEE Symposium on Logic in Computer Science, pp. 198–203. IEEE Computer Society (1989)

    Google Scholar 

  24. Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103–112 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  25. Kopylov, A.: Dependent intersection: A new way of defining records in type theory. In: LICS, pp. 86–95. IEEE Computer Society (2003)

    Google Scholar 

  26. Kopylov, A.: Type Theoretical Foundations for Data Structures, Classes, and Objects. PhD thesis, Cornell University, Ithaca, NY (2004)

    Google Scholar 

  27. Kreitz, C.: The Nuprl Proof Development System, Version 5, Reference Manual and User’s Guide. Cornell University, Ithaca, NY (2002), http://www.nuprl.org/html/02cucs-NuprlManual.pdf

  28. Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133–169 (1998)

    Article  Google Scholar 

  29. Leroy, X.: Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In: 33rd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 42–54. ACM (2006)

    Google Scholar 

  30. Li, G.: Formal Verification of Programs and Their Transformations. PhD thesis, University of Utah (2010)

    Google Scholar 

  31. McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3(4), 184–195 (1960)

    Article  MATH  Google Scholar 

  32. Mendler, P.F.: Inductive Definition in Type Theory. PhD thesis, Cornell University, Ithaca, NY (1988)

    Google Scholar 

  33. Rahli, V., Schiper, N., Renesse, R.V., Bickford, M., Constable, R.L.: A diversified and correct-by-construction broadcast service. In: The 2nd Int’l Workshop on Rigorous Protocol Engineering (WRiPE), Austin, TX (October 2012)

    Google Scholar 

  34. Schiper, N., Rahli, V., Van Renesse, R., Bickford, M., Constable, R.L.: ShadowDB: A replicated database on a synthesized consensus core. In: Eighth Workshop on Hot Topics in System Dependability, HotDep 2012 (2012)

    Google Scholar 

  35. Smith, S.F.: Partial Objects in Type Theory. PhD thesis, Cornell University, Ithaca, NY (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cornell University, Ithaca, NY, USA

    Vincent Rahli, Mark Bickford & Abhishek Anand

Authors
  1. Vincent Rahli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mark Bickford
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Abhishek Anand
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IRISA, Université Rennes 1, Campus de Beaulieu, 35042, Rennes Cedex, France

    Sandrine Blazy

  2. Université Paris-Sud, LRI, Bat 650, Univ. Paris Sud, 91405, Orsay Cedex, France

    Christine Paulin-Mohring

  3. Inria Rennes-Bretagne Atlantique, Campus de Beaulieu, 35042, Rennes Cedex, France

    David Pichardie

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rahli, V., Bickford, M., Anand, A. (2013). Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds) Interactive Theorem Proving. ITP 2013. Lecture Notes in Computer Science, vol 7998. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39634-2_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-39634-2_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-39633-5

  • Online ISBN: 978-3-642-39634-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation