Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Luo, Yong (2005)
Publisher: UKC
Languages: English
Types: Book
Subjects: QA76
Only can totally defined functions be introduced in conventional dependently typed systems and such functions are normally defined by eliminators. Because of the limitation of the elimination rules, many (mathematical) functions cannot be defined in these systems. This paper argues that the restriction of totality is unnecessary, and proposes a type theory that allows partially defined functions. In this type theory, functions can be introduced by means of pattern matching. It is in general undecidable in dependently typed systems whether patterns cover all the canonical objects of a type, and it is one of the big problems for implementation. Without the restriction of totality, we don't have such problem of totality checking, and hence we have more flexibility to introduce functions than we do in conventional type systems.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [Alt93] Th. Altenkirch. Constructions, Inductive Types and Strong Normalization . PhD thesis, Edinburgh University, 1993.
    • [B+00] B. Barras et al. The Coq Proof Assistant Reference Manual (Version 6.3.1) . INRIA-Rocquencourt, 2000.
    • [Bar84] H.P. Barendregt. The Lambda Calculus: its Syntax and Semantics. NorthHolland, revised edition, 1984.
    • [Bar92] H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Clarendon Press, 1992.
    • [C+86] R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Pretice-Hall, 1986.
    • [Coq92] Th. Coquand. Pattern matching with dependent types. Talk given at the BRA workshop on Proofs and Types, Bastad, 1992.
    • [Geu93] Herman Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993.
    • [Gog94] H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994.
    • [HHP87] R. Harper, F. Honsell, and G. Plotkin. A framework for dening logics. Proc. 2nd Ann. Symp. on Logic in Computer Science. IEEE, 1987.
    • [HHP92] R. Harper, F. Honsell, and G. Plotkin. A framework for dening logics. Journal of ACM, 40(1):143184, 1992.
    • [LP92] Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. LFCS Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, 1992.
    • [Luo90] Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. Also as Report CST-65-90/ECS-LFCS-90-118, Department of Computer Science, University of Edinburgh.
    • [Luo94] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science . Oxford University Press, 1994.
    • [Luo03] Z. Luo. pal+: a lambda-free logical framework. Journal of Functional Programming, 13(2):317338, 2003.
    • [Luo04] Y. Luo. Coherence and Transitivity in Coercive Subtyping . PhD thesis, Department of Computer Science, University of Durham, 2004.
    • [Luo05a] Y. Luo. New eta-reduction and Church-Rosser. http://www.cs.kent.ac.uk/people/sta/yl41/ , 2005.
    • [Luo05b] Y. Luo. Yet Another Normalisation Proof for Martin-Lf's Logical FrameworkTerms with correct arities are strongly normalising. http://www.cs.kent.ac.uk/people/sta/yl41/ , 2005.
    • [ML84] P. Martin-Lf. Intuitionistic Type Theory. Bibliopolis, 1984.
    • [MM04] C. McBride and J. McKinna. The view from the left. Journal of Functional Programming, 14(1):69111, 2004.
    • [MTH90] R. Milner, M. Tofte, and R. Harper. The Denition of Standard ML . MIT, 1990.
    • [MW96] P. Mellies and B. Werner. A generic normalisation proof for pure type systems, 1996.
    • [Nip01] Tobias Nipkow. More Church-Rosser proofs (in Isabelle/HOL). Journal of Automated Reasoning, 26:5166, 2001.
    • [NPS90] B. Nordstrm, K. Petersson, and J. Smith. Programming in Martin-Lf 's Type Theory: An Introduction. Oxford University Press, 1990.
    • [Tak95] Masako Takahashi. Parallel redeuctions in λ-calculus. Journal of Information and Computation, 118:120127, 1995.
    • [Tho99] Simon Thompson. Haskell : the craft of functional programming. Harlow : Addison Wesley, 2nd edition, 1999.
    • [Wer92] B. Werner. A normalization proof for an impredicative type system with large eliminations over integers. In Workshop on Logical Frameworks, 1992.
  • No related research data.
  • No similar publications.

Share - Bookmark

Download from

Cite this article