Abstract
We present a foundational framework, which we call D, unifying a lazy programming language with an impredicative constructive set theory IZF R by means of dependent types. We show that unification brings many benefits to both worlds. First, D supports two paramount paradigms of creating reliable software: correctness by construction and post-construction verification, while retaining the expressiveness of set theory. Second, D provides new expressive power, which makes it possible to internalize and prove inside D the standard meta-theoretic properties of constructive systems, such as Numerical Existence Property and Program Extraction. Finally, computation arising from the programming language significantly enriches set theory, as we show that D is stronger than IZF R and that its real numbers behave in a better way.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)
Constable, R.L.: The structure of Nuprl’s type theory. In: Logic of Computation. Series F: Computer and Systems Sciences, vol. 157, pp. 123–156. Springer, Heidelberg (1997)
The Coq Development Team: The Coq Proof Assistant Reference Manual – Version V8.0 (2004)
Benl, H., Berger, U., Schwichtenberg, H., et al.: Proof theory at work: Program development in the Minlog system. In: Bibel, W., Schmitt, P.G. (eds.) Automated Deduction, vol. II, pp. 41–71. Kluwer, Dordrecht (1998)
Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, New York (1996)
Constable, R., Moczydłowski, W.: Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 162–176. Springer, Heidelberg (2006)
Moczydłowski, W.: Investigations on Sets and Types. Ph.D thesis, Cornell University (2007)
Myhill, J.: Some properties of intuitionistic Zermelo-Fraenkel set theory. In: Cambridge Summer School in Mathematical Logic, vol. 29, pp. 206–231. Springer, Heidelberg (1973)
Moczydłowski, W.: A Normalizing Intuitionistic Set Theory with Inaccessible Sets. Logical Methods in Computer Science 3 (2007)
McCarty, D.: Realizability and Recursive Mathematics. D.Phil. Thesis, University of Oxford (1984)
Moczydłowski, W.: Normalization of IZF with Replacement. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 516–530. Springer, Heidelberg (2006)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Sørensen, M., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier, Amsterdam (2006)
Moczydłowski, W.: A Dependent Set Theory. In: Proceedings of LICS 2007, pp. 23–34. IEEE Computer Society Press, Los Alamitos (2007)
Aczel, P., Rathjen, M.: Notes on constructive set theory. Technical Report 40, Institut Mittag-Leffler (The Royal Swedish Academy of Sciences) (2000/2001)
Lubarsky, R.S.: On the Cauchy Completeness of the Constructive Cauchy Reals. Electron. Notes Theor. Comput. Sci. 167, 225–254 (2007)
Fourman, M.P., Hyland, J.: Sheaf models for analysis. In: Applications of Sheaves, pp. 280–301. Springer, Heidelberg (1979)
Pollack, R.: The Theory of LEGO:A Proof Checker for the Extended Calculus of Constructions. Ph.D thesis, Department of Computer Science, University of Edinburgh (1995)
Howe, D.J., Stoller, S.D.: An Operational Approach to Combining Classical Set Theory and Functional Programming Languages. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 36–55. Springer, Heidelberg (1994)
Grue, K.: Map theory. Theor. Comput. Sci. 102(1), 1–133 (1992)
Aczel, P.: The type theoretic interpretation of constructive set theory. In: Logic Colloquium 1977, pp. 55–66. North Holland, Amsterdam (1978)
Dowek, G., Miquel, A.: Cut elimination for Zermelo’s set theory (2006); Manuscript, available from the web pages of the authors
Shirahata, M.: Linear Set Theory. Ph.D thesis, Stanford University (1994)
Terui, K.: Light affine set theory: A naive set theory of polynomial time. Studia Logica 77(1), 9–40 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moczydłowski, W. (2008). Unifying Sets and Programs via Dependent Types. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2009. Lecture Notes in Computer Science, vol 5407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92687-0_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-92687-0_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-92686-3
Online ISBN: 978-3-540-92687-0
eBook Packages: Computer ScienceComputer Science (R0)