Type-level Computation Using Narrowing in Ωmega
Open Access
- 4 June 2007
- journal article
- Published by Elsevier BV in Electronic Notes in Theoretical Computer Science
- Vol. 174 (7), 105-128
- https://doi.org/10.1016/j.entcs.2006.10.040
Abstract
No abstract availableKeywords
This publication has 11 references indexed in Scilit:
- Combining programming with theorem provingPublished by Association for Computing Machinery (ACM) ,2005
- Evaluation strategies for functional logic programmingJournal of Symbolic Computation, 2005
- Languages of the futureACM SIGPLAN Notices, 2004
- A type system for certified binariesACM SIGPLAN Notices, 2002
- The size-change principle for program terminationACM SIGPLAN Notices, 2001
- A Finite Axiomatization of Inductive-Recursive DefinitionsLecture Notes in Computer Science, 1999
- System Description: Twelf — A Meta-Logical Framework for Deductive SystemsLecture Notes in Computer Science, 1999
- Intensional polymorphism in type-erasure semanticsACM SIGPLAN Notices, 1998
- Cayenne—a language with dependent typesACM SIGPLAN Notices, 1998
- Inductive definitions and type theory an introduction (preliminary version)Lecture Notes in Computer Science, 1994