Sciweavers

TPHOL
1997
IEEE

Higher Order Quotients and their Implementation in Isabelle HOL

13 years 7 months ago
Higher Order Quotients and their Implementation in Isabelle HOL
This paper describes the concept of higher order quotients and an implementation in Isabelle. Higher order quotients are a generalization of quotients. They use partial equivalence relations (PERs) instead of equivalence relations to group together di erent elements. This makes them applicable to arbitrary function spaces. Higher order quotients are conservatively implemented in the Isabelle logic HOL with a type constructor and a type class for PERs. Ordinary quotients are a special case of higher order quotients. An example shows how they can be used in Isabelle.
Oscar Slotosch
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1997
Where TPHOL
Authors Oscar Slotosch
Comments (0)