Title: Extensional constructs in intensional type theory
First published: 1997
Subjects: Type theory, Functional programming (Computer science), Automatic theorem proving
LC classification: QA76.9.A96 H64 1997