From Proposition to Program

• 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