Elimination with a Motive
- 14 February 2002
- book chapter
- Published by Springer Nature
- p. 197-216
- https://doi.org/10.1007/3-540-45842-5_13
Abstract
No abstract availableKeywords
This publication has 10 references indexed in Scilit:
- Extensional equality in intensional type theoryPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Inverting inductively defined relations in LEGOPublished by Springer Nature ,1998
- Deliverables: a categorical approach to program development in type theoryPublished by Springer Nature ,1993
- Unification under a mixed prefixJournal of Symbolic Computation, 1992
- Inductive sets and families in Martin-Löf's type theory and their set-theoretic semanticsPublished by Cambridge University Press (CUP) ,1991
- Telescopic mappings in typed lambda calculusInformation and Computation, 1991
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple UnificationJournal of Logic and Computation, 1991
- Inductively defined typesLecture Notes in Computer Science, 1990
- Views: a way for pattern matching to cohabit with data abstractionPublished by Association for Computing Machinery (ACM) ,1987
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965