Skip to main content
SpringerLink
Log in

Representing unification in a logical framework

  • Conference paper
  • First Online:
Computer Science Logic (CSL 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1092))

Included in the following conference series:

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. P. Barendregt. The Lambda Calculus, its syntax and semantics. North Holland, 1984.

    Google Scholar 

  2. R. Boyer and J. Moore. A Computational Logic. Academic Pres, 1979.

    Google Scholar 

  3. Jason Brown and Eike Ritter. λπ-calculus with type similarity. Technical Report PRG-TR-1-95, Oxford University Computing Laboratory, January 1995.

    Google Scholar 

  4. Jason Brown. Presentations of Unification in a Logical Framework. DPhil thesis, University of Oxford, submitted January 1996.

    Google Scholar 

  5. N. G. de Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. In M. Laudet, editor, Proceedings of the Symposium on Automatic Demonstration, pages 29–61, Versailles, France, December 1968. Springer-Verlag LNM 125.

    Google Scholar 

  6. N. G. de Bruijn. A plea for weaker frameworks. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 149–181. Cambridge University Press, 1991.

    Google Scholar 

  7. R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.

    Google Scholar 

  8. Conal Elliott. Higher-order unification with dependent type functions. In N. Dershowitz, editor, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, volume 355 of LNCS, pages 121–136. Springer-Verlag, 1989.

    Google Scholar 

  9. Conal Elliott. Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University, 1990.

    Google Scholar 

  10. Herman Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993.

    Google Scholar 

  11. M. Gordon, R, Milner and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. In volume 78 of LNCS. Springer-Verlag, 1979.

    Google Scholar 

  12. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, January 1993.

    Google Scholar 

  13. Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

    Google Scholar 

  14. Gérard Huet and Gordon Plotkin, editors. Logical Frameworks. Cambridge University Press, Cambridge, 1991.

    Google Scholar 

  15. Gerard Huet and Gordon Plotkin, editors. Logical Environments. Cambridge University Press, Cambridge, 1993.

    Google Scholar 

  16. D. Jensen and T. Pietrzykowski. Mechanizing w-order type theory through unification. Theoretical Computer Science, 3(1):123–171, 1976.

    Google Scholar 

  17. R. Letz, J. Schumann, S. Boyerl and W. Bibel. SETHEO: a high-performance theorem prover. Journal of Automated Reasoning, 8(2):183–212, 1992.

    Google Scholar 

  18. Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.

    Google Scholar 

  19. L. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–386. Academic Press, 1990.

    Google Scholar 

  20. Frank Pfenning. Logic Programming in the LF logical framework. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 149–181. Cambridge University Press, 1991.

    Google Scholar 

  21. David Pym. Proofs, Search and Computation in General Logic. PhD thesis, Laboratory for the Foundations of Computer Science University of Edinburgh, 1990. Available as technical report no. CST-69-90.

    Google Scholar 

  22. David Pym. A unification algorithm for the λπ-Calculus. International Journal of Foundations of Computer Science, 3(3):333–378, 1992.

    Google Scholar 

  23. David Pym and Lincoln Wallen. Proof search in the λπ-calculus. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 309–340. Cambridge University Press, 1991.

    Google Scholar 

  24. A. Salvesen. The Church-Rosser property for βη-reduction. Manuscript, 1991. p

    Google Scholar 

  25. Wayne Snyder. A proof theory for general unification. Birkhauser, 1991.

    Google Scholar 

  26. Wayne Snyder and Jean Gallier. Higher-order unification revisited: Complete sets of transformations. Journal of Symbolic Computation, 8:101–140, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Wolfson Building, Oxford University Computing Laboratory, Parks Road, 0X1 3QD, Oxford, UK

    Jason Brown & Lincoln A. Wallen

Authors
  1. Jason Brown
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lincoln A. Wallen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hans Kleine Büning

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brown, J., Wallen, L.A. (1996). Representing unification in a logical framework. In: Kleine Büning, H. (eds) Computer Science Logic. CSL 1995. Lecture Notes in Computer Science, vol 1092. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61377-3_34

Download citation

  • DOI: https://doi.org/10.1007/3-540-61377-3_34

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61377-0

  • Online ISBN: 978-3-540-68507-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation