A computer-verified monadic functional implementation of the integral. (English) Zbl 1209.68108
Summary: We provide a computer-verified exact monadic functional implementation of the Riemann integral in type theory. Together with previous work by O’Connor, this may be seen as the beginning of the realization of Bishop’s vision to use constructive mathematics as a programming language for exact analysis.
MSC:
| 68N18 | Functional programming and lambda calculus |
References:
| [1] | B. Aydemir, A. Bohannon, M. Fairbairn, J. Foster, B. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, S. Zdancewic, Mechanized metatheory for the masses: the POPLmark challenge, in: Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005, 2005.; B. Aydemir, A. Bohannon, M. Fairbairn, J. Foster, B. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, S. Zdancewic, Mechanized metatheory for the masses: the POPLmark challenge, in: Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005, 2005. · Zbl 1152.68516 |
| [2] | Andrej Bauer, Efficient computation with dedekind reals, Extended abstract for CCA2008, 2008.; Andrej Bauer, Efficient computation with dedekind reals, Extended abstract for CCA2008, 2008. |
| [3] | Bertot, Yves; Castéran, Pierre, Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions, (Texts in Theoretical Computer Science (2004), Springer Verlag) · Zbl 1069.68095 |
| [4] | Barthe, Gilles; Capretta, Venanzio; Pons, Olivier, Setoids in type theory, J. Funct. Programming, 13, 2, 261-293 (2003), Special issue on “Logical frameworks and metalanguages” · Zbl 1060.03030 |
| [5] | Beck, J., Distributive laws, (Eckman, B., Seminar on Triples and Categorical Homology Theory. Seminar on Triples and Categorical Homology Theory, Lecture Notes in Mathematics, vol. 80 (1969), Springer: Springer Berlin), 119-140 · Zbl 0186.02902 |
| [6] | Berger, Ulrich, From coinductive proofs to exact real arithmetic, (Computer Science Logic (2009), Springer), 132-146 · Zbl 1218.03035 |
| [7] | Bishop, Errett A., Foundations of Constructive Analysis (1967), McGraw-Hill Publishing Company, Ltd. · Zbl 0183.01503 |
| [8] | Bishop, Errett, Mathematics as a numerical language, (Intuitionism and Proof Theory (Proceedings of the summer Conference at Buffalo, N.Y., 1968) (1970), North-Holland: North-Holland Amsterdam), 53-71 · Zbl 0361.02001 |
| [9] | Andrew J. Bromage, Thomas Jäger, Lambdabot, 2006. http://www.cse.unsw.edu.au/ dons/lambdabot.html; Andrew J. Bromage, Thomas Jäger, Lambdabot, 2006. http://www.cse.unsw.edu.au/ dons/lambdabot.html |
| [10] | Bauer, Andrej; Kavkler, Iztok, A constructive theory of continuous domains suitable for implementation, Ann. Pure Appl. Logic, 159, 3, 251-267 (2009) · Zbl 1169.06005 |
| [11] | Barr, Michael; Wells, Charles, Toposes, triples and theories, Repr. Theory Appl. Categ., 12 (2005), x+288 pp. Corrected reprint of the 1985 original [MR0771116] · Zbl 1081.18006 |
| [12] | Cruz-Filipe, L., A constructive formalization of the fundamental theorem of calculus, (Geuvers, H.; Wiedijk, F., Types for Proofs and Programs. Types for Proofs and Programs, LNCS, vol. 2646 (2003), Springer-Verlag), 108-126 · Zbl 1023.03059 |
| [13] | L. Cruz-Filipe, Constructive real analysis: a type-theoretical formalization and applications, Ph.D. Thesis, University of Nijmegen, April 2004.; L. Cruz-Filipe, Constructive real analysis: a type-theoretical formalization and applications, Ph.D. Thesis, University of Nijmegen, April 2004. |
| [14] | Cruz-Filipe, L.; Geuvers, H.; Wiedijk, F., C-corn: the constructive Coq repository at Nijmegen, (Asperti, A.; Bancerek, G.; Trybulec, A., Mathematical Knowledge Management, Third International Conference. Mathematical Knowledge Management, Third International Conference, MKM 2004. Mathematical Knowledge Management, Third International Conference. Mathematical Knowledge Management, Third International Conference, MKM 2004, LNCS, vol. 3119 (2004), Springer-Verlag), 88-103 · Zbl 1108.68586 |
| [15] | Cruz-Filipe, L.; Spitters, B., Program extraction from large proof developments, (Basin, D.; Wolff, B., Theorem Proving in Higher Order Logics, 16th International Conference. Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003. Theorem Proving in Higher Order Logics, 16th International Conference. Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, LNCS, vol. 2758 (2003), Springer-Verlag), 205-220 · Zbl 1279.68287 |
| [16] | Coquand, Thierry; Huet, Gérard, The calculus of constructions, Inform. and Comput., 76, 2-3, 95-120 (1988) · Zbl 0654.03045 |
| [17] | Coen, Claudio Sacerdoti, A semi-reflexive tactic for (sub-)equational reasoning, (Filliâtre, Jean-Christophe; Paulin-Mohring, Christine; Werner, Benjamin, TYPES. TYPES, Lecture Notes in Computer Science, vol. 3839 (2004), Springer), 98-114 · Zbl 1172.68614 |
| [18] | Coquand, Thierry; Paulin, Christine, Inductively defined types, (COLOG-88. COLOG-88, Tallinn, 1988. COLOG-88. COLOG-88, Tallinn, 1988, Lecture Notes in Comput. Sci., vol. 417 (1990), Springer: Springer Berlin), 50-66 · Zbl 0722.03006 |
| [19] | Edalat, Abbas, Numerical integration with exact real arithmetic, (Automata, Languages and Programming, 26th International Colloquium. Automata, Languages and Programming, 26th International Colloquium, ICALP99, Prague, Czech 227 Republic, July 11-15, 1999, Proceedings. Automata, Languages and Programming, 26th International Colloquium. Automata, Languages and Programming, 26th International Colloquium, ICALP99, Prague, Czech 227 Republic, July 11-15, 1999, Proceedings, Lecture Notes in Computer Science, vol. 1644 (1999), Springer), 90-104 · Zbl 0937.65025 |
| [20] | Benjamin Grégoire, Xavier Leroy, A compiled implementation of strong reduction, in: ICFP, 2002, pp. 235-246.; Benjamin Grégoire, Xavier Leroy, A compiled implementation of strong reduction, in: ICFP, 2002, pp. 235-246. · Zbl 1322.68053 |
| [21] | Geuvers, Herman; Niqui, Milad; Spitters, Bas; Wiedijk, Freek, Constructive analysis, types and exact real numbers (overview article), Mathematical Structures in Computer Science, 17, 1, 3-36 (2007) · Zbl 1157.03036 |
| [22] | Hofmann, Martin, Extensional constructs in intensional type theory, (CPHC/BCS Distinguished Dissertations (1997), Springer-Verlag London Ltd: Springer-Verlag London Ltd London) · Zbl 1411.03001 |
| [23] | Mark P. Jones, Luke Duponcheel, Composing monads, Technical Report YALEU/DCS/RR-1004, Yale University, 1993.; Mark P. Jones, Luke Duponcheel, Composing monads, Technical Report YALEU/DCS/RR-1004, Yale University, 1993. |
| [24] | Cezary Kaliszyk, Russell O’Connor, Computing with classical real numbers, Journal of Automated Reasoning, 2008 (Submitted for publication).; Cezary Kaliszyk, Russell O’Connor, Computing with classical real numbers, Journal of Automated Reasoning, 2008 (Submitted for publication). · Zbl 1194.68097 |
| [25] | Lang, Serge, Real and Functional Analysis (1993), Springer · Zbl 0831.46001 |
| [26] | Martin-Löf, Per, Constructive mathematics and computer programming, (Logic, methodology and philosophy of science, VI. Logic, methodology and philosophy of science, VI, Hannover, 1979. Logic, methodology and philosophy of science, VI. Logic, methodology and philosophy of science, VI, Hannover, 1979, Stud. Logic Found. Math., vol. 104 (1982), North-Holland: North-Holland Amsterdam), 153-175 · Zbl 0541.03034 |
| [27] | Martin-Löf, Per, An intuitionistic theory of types, (Twenty-five years of constructive type theory. Twenty-five years of constructive type theory, Venice, 1995. Twenty-five years of constructive type theory. Twenty-five years of constructive type theory, Venice, 1995, Oxford Logic Guides, vol. 36 (1998), Oxford Univ. Press), 127-172 · Zbl 0931.03070 |
| [28] | McBride, Conor; McKinna, James, The view from the left, Journal of Functional Programming, 14, 1, 69-111 (2004) · Zbl 1069.68539 |
| [29] | Moggi, E., Computational lambda-calculus and monads, (Proceedings of the Fourth Annual Symposium on Logic in computer science (1989), IEEE Press: IEEE Press Piscataway, NJ, USA), 14-23 · Zbl 0716.03007 |
| [30] | McBride, Conor; Paterson, Ross, Applicative programming with effects, J. Funct. Program., 18, 1, 1-13 (2008) · Zbl 1128.68020 |
| [31] | Nordström, Bengt; Petersson, Kent; Smith, Jan M., Programming in Martin-Löf’s type theory, (International Series of Monographs on Computer Science, vol. 7 (1990), The Clarendon Press Oxford University Press: The Clarendon Press Oxford University Press New York), An introduction · Zbl 0744.03029 |
| [32] | O’Connor, Russell, A monadic, functional implementation of real numbers, Mathematical Structures in Computer Science, 17, 1, 129-159 (2007) · Zbl 1121.03024 |
| [33] | O’Connor, Russell, Certified exact transcendental real number computation in Coq, (Ait-Mohamed, Otmane, TPHOLs. TPHOLs, Lecture Notes in Computer Science, vol. 5170 (2008), Springer), 246-261 · Zbl 1165.68466 |
| [34] | O’Connor, Russell, A computer verified theory of compact sets, (Buchberger, Bruno; Ida, Tetsuo; Kutsia, Temur, SCSS 2008. SCSS 2008, RISC-Linz Report Series, vol. 08-08 (2008), RISC: RISC Castle of Hagenberg, Austria), 148-162 |
| [35] | Richman, Fred, Real numbers and other completions, Math. Log. Q., 54, 1, 98-108 (2008) · Zbl 1134.03041 |
| [36] | Sambin, Giovanni, Intuitionistic formal spaces — a first communication, (Skordev, D., Mathematical Logic and Its Applications (1987), Plenum), 187-204 · Zbl 0703.03040 |
| [37] | Schröder, L., Expressivity of coalgebraic modal logic: the limits and beyond, (Sassone, V., Foundations of Software Science and Computational Structures. Foundations of Software Science and Computational Structures, Lecture Notes in Mathematics, vol. 3441 (2005), Springer: Springer Berlin), 440-454 · Zbl 1119.03015 |
| [38] | Schwichtenberg, Helmut, Realizability interpretation of proofs in constructive analysis, Theor. Comp. Sys., 43, 3, 583-602 (2008) · Zbl 1166.03035 |
| [39] | Simpson, Alex K., Lazy functional algorithms for exact real functionals, Lecture Notes in Computer Science, 1450, 456-464 (1998) · Zbl 0913.65009 |
| [40] | Sörensen, M.; Urzyczyn, P., Lectures on the Curry-Howard Isomorphism (1998), Elsevier · Zbl 1183.03004 |
| [41] | The Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, 2008.; The Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, 2008. |
| [42] | Thompson, S., Type Theory and Functional Programming (1991), Addison Wesley · Zbl 0753.68026 |
| [43] | P. Wadler, Monads for functional programming, in: Proceedings of the Marktoberdorf Summer School on Program Design Calculi, August 1992.; P. Wadler, Monads for functional programming, in: Proceedings of the Marktoberdorf Summer School on Program Design Calculi, August 1992. · Zbl 0798.68040 |
| [44] | Wadler, Philip, Comprehending monads, Mathematical Structures in Computer Science, 2, 4, 461-493 (1992) · Zbl 0798.68040 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
