Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Functional and Logic Programming

FLOPS 2016: Functional and Logic Programming pp 29–44Cite as

From Proposition to Program

Embedding the Refinement Calculus in Coq

  • Conference paper
  • First Online:

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

Abstract

The refinement calculus and type theory are both frameworks that support the specification and verification of programs. This paper presents an embedding of the refinement calculus in the interactive theorem prover Coq, clarifying the relation between the two. As a result, refinement calculations can be performed in Coq, enabling the semi-automatic calculation of formally verified programs from their specification.

This is a preview of subscription content, 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 EPUB and 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

Learn about institutional subscriptions

References

  • Altenkirch, T., Morris, P.: Indexed containers. In: 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, pp. 227–285 (2009)

    Google Scholar 

  • Back, R.J.R., von Wright, J.: Refinement concepts formalized in higher order logic. Formal Aspects Comput. 2, 247–272 (1989)

    Article  MATH  Google Scholar 

  • Von Wright, J.: Refinement Calculus: Refinement Calculus. Texts in Computer Science. Springer, New York (1998)

    MATH  Google Scholar 

  • Back, R.J.R., von Wright, J.: Refinement concepts formalised in higher order logic. Formal Aspects Comput. 2(1), 247–272 (1990)

    Article  MATH  Google Scholar 

  • Back, R.J.R.: On the Correctness of Refinement in Program Development. PhD thesis, University of Helsinki (1978)

    Google Scholar 

  • Boulmé, S.: Intuitionistic refinement calculus. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 54–69. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  • Butler, M.J., Grundy, J., Långbacka, T., Ruksenas, R., Wright, J.V.: The refinement calculator. In: Formal Methods Pacific (1997)

    Google Scholar 

  • Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: International Conference on Functional Programming, ICFP 2009, pp. 79–90 (2009)

    Google Scholar 

  • Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    Google Scholar 

  • Dongol, B., Gomes, V.B.F., Struth, G.: A program construction and verification tool for separation logic. In: Hinze, R., Voigtländer, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 137–158. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  • Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci 19(19–32), 1 (1967)

    MathSciNet  MATH  Google Scholar 

  • Hancock, P., Hyvernat, P.: Programming interfaces and basic topology. Ann. Pure Appl. Logic 137(1), 189–239 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  • Setzer, A., Hancock, P.: Interactive programs in dependent type theory. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. lncs, vol. 1862, pp. 317–339. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  • Hancock, P., Setzer, A.: Specifying interactions with dependent types. In: Workshop on subtyping and dependent types in programming (2000b)

    Google Scholar 

  • Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  • Morgan, C.: Programming from specifications. Prentice-Hall Inc, Upper Saddle River (1990)

    Google Scholar 

  • Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Dependent types for imperative programs. In: International Conference on Functional Programming, ICFP 2008, pp. 229–240 (2008)

    Google Scholar 

  • Flemming, N., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)

    MATH  Google Scholar 

  • Swierstra, W.: A hoare logic for the state monad. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 440–451. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  • Swierstra, W.: A functional specification of effects. PhD thesis, University of Nottingham (2009)

    Google Scholar 

  • Swierstra, W., Altenkirch, T.: Beauty in the beast: In: Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop, pp. 25-36. ACM (2007)

    Google Scholar 

Download references

Acknowledgments

The first author would like to thank Peter Hancock for his patience in explaining the relation between interaction structures and the refinement calculus. The first author’s visit to Scotland was funded by the London Mathematical Society’s Scheme 7 grant.

Author information

Authors and Affiliations

  1. Universiteit Utrecht, Utrecht, The Netherlands

    Wouter Swierstra

  2. RiskCo, Utrecht, The Netherlands

    Joao Alpuim

Authors
  1. Wouter Swierstra
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joao Alpuim
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wouter Swierstra .

Editor information

Editors and Affiliations

  1. Tohoku University, Sendai, Japan

    Oleg Kiselyov

  2. School of Computing, University of Kent, Canterbury, United Kingdom

    Andy King

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Swierstra, W., Alpuim, J. (2016). From Proposition to Program. In: Kiselyov, O., King, A. (eds) Functional and Logic Programming. FLOPS 2016. Lecture Notes in Computer Science(), vol 9613. Springer, Cham. https://doi.org/10.1007/978-3-319-29604-3_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-29604-3_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29603-6

  • Online ISBN: 978-3-319-29604-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation