×

Type-level computation using narrowing in \(\Omega\)mega. (English) Zbl 1277.68046

Stump, Aron (ed.) et al., Proceedings of the programming languages meets program verification (PLPV 2006), Seattle, WA, USA, August 21, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 7, 105-128 (2007).
Summary: \(\Omega\)mega is an experimental system that combines features of both a programming language and a logical reasoning system. \(\Omega\)mega is a language with an infinite hierarchy of computational levels. Terms at one level are classified (or typed) by terms at the next higher level. In this paper we report on using two different computational mechanisms. At the value level, computation is performed by reduction, and is largely unconstrained. At all higher levels, computation is performed by narrowing.
For the entire collection see [Zbl 1273.68046].

MSC:

68N15 Theory of programming languages
03B70 Logic in computer science
68N18 Functional programming and lambda calculus
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Cayenne; Epigram; Twelf; LEGO; Coq
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Antoy, S., Definitional trees, (Kirchner, H.; Levi, G., Proc. of the 3rd International Conference on Algebraic and Logic Programming. Proc. of the 3rd International Conference on Algebraic and Logic Programming, Volterra, Italy. Proc. of the 3rd International Conference on Algebraic and Logic Programming. Proc. of the 3rd International Conference on Algebraic and Logic Programming, Volterra, Italy, LNCS, vol. 632 (September 1992), Springer), 143-157
[2] Antoy, S.; Ariola, Z. M., Narrowing the narrowing space, (9th International Symposium on Programming Languages, Implementations, Logics, and Programs. 9th International Symposium on Programming Languages, Implementations, Logics, and Programs, (PLILP’97). 9th International Symposium on Programming Languages, Implementations, Logics, and Programs. 9th International Symposium on Programming Languages, Implementations, Logics, and Programs, (PLILP’97), Lecture Notes in Computer Science, 1292 (1997)), 1
[3] Antoy, Sergio, Evaluation strategies for functional logic programming, Journal of Symbolic Computation, 40, 1, 875-903 (July 2005)
[4] Augustsson, Lennart, Cayenne — a language with dependent types, ACM SIGPLAN Notices, 34, 1, 239-250 (January 1999)
[5] Lennart Augustsson. Equality proofs in cayenne, July 11 2000; Lennart Augustsson. Equality proofs in cayenne, July 11 2000
[6] Boyer, Robert S.; Moore, J. Strother, A Computational Logic (1979), Academic Press: Academic Press New York · Zbl 0448.68020
[7] Jürgen Brauburger. Automatic Termination Analysis for Functional and Imperative Programs; Jürgen Brauburger. Automatic Termination Analysis for Functional and Imperative Programs · Zbl 0979.68016
[8] Cardelli, Luca; Wegner, Peter, On understanding types, data abstraction and polymorphism, ACMCS, 17, 4, 471-522 (December 1985)
[9] Chen and Xi. Combining programming with theorem proving. In Proceedings of the 2005 ACM/SIGPLAN International Conference on Functional Programming (ICFP’05); Chen and Xi. Combining programming with theorem proving. In Proceedings of the 2005 ACM/SIGPLAN International Conference on Functional Programming (ICFP’05) · Zbl 1302.68241
[10] Chen, Chiyan; Xi, Hongwei, Combining programming with theorem proving, (ICFP 2005 (2005)) · Zbl 1302.68241
[11] Coquand, Catarina, Agda is a system for incrementally developing proofs and programs, Web page describing AGDA: · Zbl 1041.68016
[12] Coquand, T.; Dybjer, P., Inductive definitions and type theory an introduction, Lecture Notes in Computer Science, 880, 60-76 (1994), (preliminary version) · Zbl 1044.03521
[13] Karl Crary, Stephanie Weirich, and J. Gregory Morrisett, Intensional polymorphism in type-erasure semantics. In ICFP; Karl Crary, Stephanie Weirich, and J. Gregory Morrisett, Intensional polymorphism in type-erasure semantics. In ICFP · Zbl 1370.68046
[14] Davies, Rowan, A refinement-type checker for Standard ML, (International Conference on Algebraic Methodology and Software Technology. International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, volume 1349 (1997), Springer-Verlag) · Zbl 1426.68034
[15] Dybjer, P.; Setzer, A., A finite axiomatization of inductive-recursive definitions, Lecture Notes in Computer Science, 1581, 129-146 (1999) · Zbl 0931.03069
[16] Hanus, Michael; Sadre, Ramin, An abstract machine for curry and its concurrent implementation in java, Journal of Functional and Logic Programming, 1999, Special Issue 1 (1999)
[17] Hanus, M., Curry: An integrated functional logic language (vers. 0.8.2) (March 28, 2006), Available at
[18] Peyton Jones, Simon; Shields, Mark, Practical type inference for arbitrary-rank types (2003), Technical report, Microsoft Research, “December” · Zbl 1107.68030
[19] Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In POPL; Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In POPL · Zbl 1323.68216
[20] Zhaohui Luo and Robert Pollack. LEGO proof development system: User’s manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, The King’s Buildings, Edinburgh EH9 3JZ, May 1992. Updated version; Zhaohui Luo and Robert Pollack. LEGO proof development system: User’s manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, The King’s Buildings, Edinburgh EH9 3JZ, May 1992. Updated version
[21] onnor McBride, C., Epigram: Practical programming with dependent types (August 2004), In Notes from the 5th International Summer School on Advanced Functional Programming. Available at:
[22] Bengt Nordstrom. The ALF proof editor, March 20 1996; Bengt Nordstrom. The ALF proof editor, March 20 1996
[23] Pasalic, Emir, The Role of Type Equality in Meta-programming (October 2004), PhD thesis, OGI School of Science & Engineering at OHSU. Available from:
[24] Pasalic, Emir; Linger, Nathan, Meta-programming with typed object-language representations, (Generative Programming and Component Engineering. Generative Programming and Component Engineering, (GPCE’04). Generative Programming and Component Engineering. Generative Programming and Component Engineering, (GPCE’04), LNCS, volume 3286 (October 2004)), 136-167
[25] Paulson, Lawrence C., Isabelle: The next 700 theorem provers, (Odifreddi, P., Logic and Computer Science (1990), Academic Press), 361-386
[26] Frank Pfenning and Carsten Schürmann. Twelf User’s Guide; Frank Pfenning and Carsten Schürmann. Twelf User’s Guide
[27] Frank Pfenning and Carsten Schürmann. System description: Twelf — A meta-logical framework for deductive systems. In Harald Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16)LNAI; Frank Pfenning and Carsten Schürmann. System description: Twelf — A meta-logical framework for deductive systems. In Harald Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16)LNAI
[28] Shao, Zhong; Saha, Bratin; Trifonov, Valery; Papaspyrou, Nikolaos, A type system for certified binaries, ACM SIGPLAN Notices, 37, 1, 217-232 (January 2002)
[29] Tim Sheard. Languages of the future. Onward Track, OOPSLA’04. Reprinted in: ACM SIGPLAN Notices, Dec 2004; Tim Sheard. Languages of the future. Onward Track, OOPSLA’04. Reprinted in: ACM SIGPLAN Notices, Dec 2004
[30] Sheard, Tim, Playing with types (2005), Technical report, Portland State University
[31] Sheard, Tim, Putting Curry-Howard to work, (Proceedings of the ACM SIGPLAN 2005 Haskell Workshop (2005)), 74-85
[32] Sheard, Tim; Hook, James; Linger, Nathan, GADTs + extensible kind system = dependent programming (2005), Technical report, Portland State University
[33] Sheard, Tim; Linger, Nathan, Programming with static invariants in omega (September 2004), Available from:
[34] Sheard, Tim; Pasalic, Emir, Meta-programming with built-in type equality (July 2004), In Logical Frameworks and Meta-Languages workshop. Available at:
[35] Christopher A. Stone and Robert Harper. Deciding type equivalence in a language with singleton kinds. In Conference Record of POPL’00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages; Christopher A. Stone and Robert Harper. Deciding type equivalence in a language with singleton kinds. In Conference Record of POPL’00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages · Zbl 1323.68163
[36] Stuckey, Peter J.; Sulzmann, Martin, Type inference for guarded recursive data types (February 2005), Available from:
[37] Stump, Aaron, Imperative LF meta-programming (July 2004), In Logical Frameworks and Meta-Languages workshop. Available at:
[38] Sulzmann, Martin; Wang, Meng, A systematic translation of guarded recursive data types to existential types (February 2005), Available from:
[39] The Coq Proof Assistant Reference Manual, Version 7.4. INRIA (2003)
[40] Westbrook, Edwin; Stump, Aaron; Wehrman, Ian, A language-based approach to functionally correct inperative programming (2005), Technical report, Washington University in St. Louis. Available at: · Zbl 1302.68095
[41] Hongwei Xi. Dependent Types in Practical Programming; Hongwei Xi. Dependent Types in Practical Programming · Zbl 1125.68033
[42] Xi, Hongwei, Applied type systems, (In post-workshop proceedingds of TYPES 2003. In post-workshop proceedingds of TYPES 2003, LNCS, 3085 (2004), Springer-Verlag), 394-408, (extended abstract) · Zbl 1100.03518
[43] Xi, Hongwei; Pfenning, Frank, Eliminating array bound checking through dependent types, ACM SIGPLAN Notices, 33, 5, 249-257 (May 1998)
[44] Xi, Hongwei; Pfenning, Frank, Dependent types in practical programming, (ACM, POPL ’99. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages. POPL ’99. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages, January 20-22, 1999, San Antonio, TX. POPL ’99. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages. POPL ’99. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages, January 20-22, 1999, San Antonio, TX, ACM SIGPLAN Notices (1999), ACM Press: ACM Press New York, NY, USA), 214-227
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.