Modular Structures as Dependent Types in Isabelle

1. R. Burstall. Computer Assisted Proof for Mathematics: an Introduction using the LEGO Proof System. Technical Report ECS-LFCS-91-132, University of Edinburgh, 1990. 131

   Google Scholar 

2. A. Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, pages 56–68, 1940. 125

   Google Scholar 

3. W. M. Farmer, J. D. Guttman, and F. J. Thayer. imps: an Interactive Mathematical Proof System. Journal of Automated Reasoning, 11:213–248, 1993. 121, 122, 123

   Article  MATH  Google Scholar 

4. John V. Guttag and James J. Horning, editors. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993. With Stephen J. Garland, Kevin D. Jones, Andrés Modet, and Jeannette M. Wing. 121, 123

   Google Scholar 

5. A. Heyting. Intuitionism: An Introduction. North Holland, Amsterdam, 1956. 125

   Google Scholar 

6. F. Kammüller and L. C. Paulson. A Formal Proof of Sylow’s First Theorem-An Experiment in Abstract Algebra with Isabelle HOL. Journal of Automated Reasoning, 1999. To appear. 121

   Google Scholar 

7. F. Kammüller and M. Wenzel. Locales-a Sectioning Concept for Isabelle. Technical Report 449, University of Cambridge, Computer Laboratory, 1998. 131

   Google Scholar 

8. Z. Luo and R. Pollack. _{Lego proof development system: User’s manual}. Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992. 131

   Google Scholar 

9. Z. Luo. A Higher-order Calculus and Theory Abstraction. Information and Computation, 90(1), 1990. 131

   Google Scholar 

10. Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. Also as Report CST-65-90. 131

    Google Scholar 

11. D. B. MacQueen. Using Dependant Types to Express Modular Structures. In Proc. 13th ACM Symp. Principles Programming Languages. ACM Press, 1986. 131

    Google Scholar 

12. B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf’ s Type Theory — An Introduction. Oxford Science Publications. Clarendon Press, Oxford, 1990. 125

    Google Scholar 

13. W. Naraschewski and M. Wenzel. Object-oriented Verification based on Record Subtyping in Higher-Order Logic. In 11th International Conference on Theorem Proving in Higher Order Logics, volume 1479 of LNCS, ANU, Canberra, Australia, 1998. Springer-Verlag. 121, 123

    Google Scholar 

14. S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language (Beta Release). Technical report, SRI International, 1993. 121, 123

    Google Scholar 

15. R. Pollack. The Tarski Fixpoint Theorem. http://e-mail to: proof-sci@se.chalmers.cs, 1990. 131

16. R. Pollack. _{Theories in Type Theory}. Slides, available on the Web as http://www.brics.dk/pollack, unknown year. 132

17. D. T. Sannella and R. M. Burstall. Structured Theories in LCF. In CAAP’83: Trees in Algebra and Programming, volume 159 of LNCS, pages 377–91. Springer-Verlag, 1983. 131

    Google Scholar 

18. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955. 130

    MATH  MathSciNet  Google Scholar 

Download references