Skip to main content
SpringerLink
Log in
Book cover

Logic, Language and Computation pp 10–30Cite as

On implicit arguments

  • Chapter
  • First Online:

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

Abstract

A typechecker for a typed λ-calculus having implicit arguments is presented. The typechecker works in such a way that the uniqueness of implicit arguments is always preserved during reduction. Consequently, when it compares two terms by reduction, it can reduce them without inferring implicit arguments. Before describing the typechecker, we analyze various situations where the uniqueness of implicit arguments is not preserved by naïvely defined reduction.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Barendregt. Introduction to generalised type systems. Journal of Functional Programming, Vol.1, No.2, pp.124–154, 1991.

    Google Scholar 

  2. V. Breazu-Tannen, T. Coquand, C. A. Gunter and A. Scedrov. Inheritance as Implicit Coercion. Information and Computation, Vol.93, No.1, pp.172–221, 1991.

    Article  Google Scholar 

  3. R. Harper and J. C. Mitchell. On the type structure of standard ML. ACM Transactions on Programming Languages and Systems, Vol.15, No.2, pp.211–252, 1993.

    Article  Google Scholar 

  4. Z. Luo and R. Pollack. LEGO proof development system: User's manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Department, University of Edinburgh, 1992.

    Google Scholar 

  5. D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, Vol.1, No.4, pp.497–536, 1991.

    Google Scholar 

  6. D. Miller. Unification of simply typed lambda-terms as logic programming. In K. Furukawa, editor, In Proceedings of the Eighth International Conference on Logic Programming, MIT Press, 1991.

    Google Scholar 

  7. D. Miller. Unification under a mixed prefix. Journal of Symbolic Computation, Vol.14, No.4, pp.321–358, 1992.

    Article  Google Scholar 

  8. F. Pfenning. Elf: A language for logic definition and verified metaprogramming. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, Asilomar, California, 1989.

    Google Scholar 

  9. F. Pfenning. Logic programming in the LF logical Framework, In Proceedings of the First Workshop on Logical Frameworks, 1991.

    Google Scholar 

  10. R. Pollack. Implicit syntax. LFCS, Computer Science Department, University of Edinburgh, 1992.

    Google Scholar 

  11. M. H. Takahashi. Parallel Reductions in λ-Calculus. Journal of Symbolic Computation, Vol.7, pp.113–123, 1989.

    Google Scholar 

  12. H. Tsuiki. A normalizing calculus with subtyping and overloading. Theoretical Aspects of Computer Software 94, Lecture Notes in Computer Science, to appear.

    Google Scholar 

  13. L. S. van Benthem Jutting. Typing in pure type systems. Information and Computation, Vol.105, pp.30–41, 1993.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Information Science, University of Tokyo, 7-3-1 Hongo, Bunkyo-ku, 113, Tokyo, Japan

    Masami Hagiya & Yozo Toda

Authors
  1. Masami Hagiya
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yozo Toda
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Neil D. Jones Masami Hagiya Masahiko Sato

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Hagiya, M., Toda, Y. (1994). On implicit arguments. In: Jones, N.D., Hagiya, M., Sato, M. (eds) Logic, Language and Computation. Lecture Notes in Computer Science, vol 792. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032392

Download citation

  • DOI: https://doi.org/10.1007/BFb0032392

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57935-9

  • Online ISBN: 978-3-540-48391-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation