Modular Reasoning in Isabelle

1. Bailey, A.: The Machine-Checked Literate Formalisation of Algebra in Type Theory. PhD thesis. University of Manchester (1998)

   Google Scholar 

2. Dowek, G. et al.: The Coq proof assistant user’s guide. Technical Report 154, INRIA-Rocquencourt (1993)

   Google Scholar 

3. de Bruijn, N.G.: A Survey of the Project AUTOMATH. In: Seldin and Hindley [SH80], pp. 579–606

   Google Scholar 

4. Dowek,G.: Naming and Scoping in a Mathematical Vernacular. Technical Report 1283, INRIA, Rocquencourt (1990)

   Google Scholar 

5. Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: an Interactive Mathematical Proof System. Journal of Automated Reasoning 11, 213–248 (1993)

   Article  MATH  Google Scholar 

6. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL, a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

   MATH  Google Scholar 

7. Gunter, E. L.: Doing Algebra in Simple Type Theory. Technical Report MS-CIS-89-38, Dep. of Computer and Information Science. University of Pennsylvania (1989)

   Google Scholar 

8. Gunter, E.L.: The Implementation and Use of Abstract Theories in HOL. In: Third HOL Users Meeting. Aarhus University (1990)

   Google Scholar 

9. Howard, W.A.: The formulae-as-types notion of construction. In: Seldin and Hindley [SH80], pp. 479–490

   Google Scholar 

10. Jacobs, B., Melham, T.F.: Translating Dependent Type Theory into Higher Order Logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664. Springer, Heidelberg (1993)

    Google Scholar 

11. Kammüller, F.: Modular Reasoning in Isabelle. PhD thesis. University of Cambridge, Technical Report 470 (1999)

    Google Scholar 

12. Kammüller, F.: Modular Structures as Dependent Types in Isabelle. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, p. 121. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

13. Kammüller, F., Paulson, L.C.: A Formal Proof of Sylow’s First Theorem – An Experiment in Abstract Algebra with Isabelle HOL. Journal of Automated Reasoning 23(3-4), 235–264 (1999)

    Article  MATH  MathSciNet  Google Scholar 

14. Kammüller, F., Wenzel, M., Paulson, L.C.: Locales – a Sectioning Concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, p. 149. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

15. Luo, Z., Pollack, R.: Lego proof development system: User’s manual. Technical Report ECS-LFCS-92-211. University of Edinburgh (1992)

    Google Scholar 

16. MacQueen, D.B.: Using Dependant Types to Express Modular Structures. In: Proc. 13th ACM Symp. Principles Programming Languages. ACM Press, New York (1986)

    Google Scholar 

17. Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Part of the PVS Manual. Available on the Web as, http://www.csl.sri.com/pvsweb/manuals.html (September 1998)

18. Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)

    MATH  Google Scholar 

19. Seldin, J.P., Hindley, J.R. (eds.): To H. B. Curry: Essays on Combinatory Logic. Academic Press Limited, London (1980)

    MATH  Google Scholar 

20. Trybulec, A.: Some Features of the Mizar Language (1993), Available from Mizar user’s group

    Google Scholar 

21. Yu, Y.: Computer Proofs in Group Theory. Journal of Automated Reasoning 6, 251–286 (1990)

    Article  MATH  MathSciNet  Google Scholar 

Download references