Strongly Typed Term Representations in Coq
- 2 March 2011
- journal article
- Published by Springer Science and Business Media LLC in Journal of Automated Reasoning
- Vol. 49 (2), 141-159
- https://doi.org/10.1007/s10817-011-9219-0
Abstract
No abstract availableKeywords
This publication has 19 references indexed in Scilit:
- Type Theory Should Eat ItselfElectronic Notes in Theoretical Computer Science, 2009
- Some Domain Theory and Denotational Semantics in CoqLecture Notes in Computer Science, 2009
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive FamilyLecture Notes in Computer Science, 2007
- Formalized Metatheory with Terms Represented by an Indexed Family of TypesLecture Notes in Computer Science, 2006
- Generalized algebraic data types and object-oriented programmingACM SIGPLAN Notices, 2005
- The view from the leftJournal of Functional Programming, 2004
- Elimination with a MotiveLecture Notes in Computer Science, 2002
- de Bruijn notation as a nested datatypeJournal of Functional Programming, 1999
- Nested datatypesLecture Notes in Computer Science, 1998
- A framework for defining logicsJournal of the ACM, 1993