Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- 1 January 2013
- book chapter
- Published by Springer Science and Business Media LLC
Abstract
No abstract availableThis publication has 11 references indexed in Scilit:
- Automatic Data RefinementLecture Notes in Computer Science, 2013
- Data Refinement in Isabelle/HOLLecture Notes in Computer Science, 2013
- Quotients revisited for Isabelle/HOLPublished by Association for Computing Machinery (ACM) ,2011
- Defining functions on equivalence classesACM Transactions on Computational Logic, 2006
- A Semi-reflexive Tactic for (Sub-)Equational ReasoningLecture Notes in Computer Science, 2006
- A Design Structure for Higher Order QuotientsLecture Notes in Computer Science, 2005
- Changing Data Representation within the Coq SystemLecture Notes in Computer Science, 2003
- Theorem Proving with the Real NumbersPublished by Springer Science and Business Media LLC ,1998
- Higher order quotients and their implementation in Isabelle HOLPublished by Springer Science and Business Media LLC ,1997
- Representation independence and data abstractionPublished by Association for Computing Machinery (ACM) ,1986