Dependently Typed Records for Representing Mathematical Structure
- 1 January 2000
- conference paper
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 462-479
- https://doi.org/10.1007/3-540-44659-1_29
Abstract
No abstract availableThis publication has 9 references indexed in Scilit:
- Dependent CoercionsElectronic Notes in Theoretical Computer Science, 1999
- Coercive subtypingJournal of Logic and Computation, 1999
- Abstract insertion sort in an extension of type theory with record types and subtypingPublished by Springer Science and Business Media LLC ,1998
- Typing algorithm in type theory with inheritancePublished by Association for Computing Machinery (ACM) ,1997
- A type-theoretic approach to higher-order modules with sharingPublished by Association for Computing Machinery (ACM) ,1994
- Manifest types, modules, and separate compilationPublished by Association for Computing Machinery (ACM) ,1994
- Telescopic mappings in typed lambda calculusInformation and Computation, 1991
- Pebble, a kernel language for modules and abstract data typesInformation and Computation, 1988
- Using dependent types to express modular structurePublished by Association for Computing Machinery (ACM) ,1986