\<^loc>\ x = \<^loc>\" by simp with assoc [symmetric] neutl invl have "x\<^loc>\

\<^loc>\ (x \<^loc>\ \<^loc>\) = x\<^loc>\

\<^loc>\ x" by simp with left_cancel show "x \<^loc>\ \<^loc>\ = x" by simp - qed *) + qed + +text {* + The logical proof is carried out on the locale level + and thus conveniently is opened using the @{text unfold_locales} + method which only leaves the logical differences still + open to proof to the user. After the proof it is propagated + to the type system, making @{text group} an instance of + @{text monoid}. For illustration, a derived definition + in @{text group} which uses @{text of_nat}: +*} + + definition (in group) + pow_int :: "int \ \ \ \" where + "pow_int k x = (if k >= 0 + then pow_nat (nat k) x + else (pow_nat (nat (- k)) x)\<^loc>\

)" + +text {* + yields the global definition of + @{term [source] "pow_int \ int \ \\group \ \\group"} + with the corresponding theorem @{thm pow_int_def [no_vars]}. +*} *) + section {* Further issues *} @@ -437,11 +482,11 @@ takes this into account. Concerning target languages lacking type classes (e.g.~SML), type classes are implemented by explicit dictionary construction. - As example, the natural power function on groups: + For example, lets go back to the power function: *} fun - pow_nat :: "nat \ \\monoidl \ \\monoidl" where + pow_nat :: "nat \ \\group \ \\group" where "pow_nat 0 x = \" | "pow_nat (Suc n) x = x \ pow_nat n x" @@ -459,19 +504,17 @@ \noindent This maps to Haskell as: *} -code_gen example in Haskell file "code_examples/" +code_gen example in Haskell to Classes file "code_examples/" (* NOTE: you may use Haskell only once in this document, otherwise you have to work in distinct subdirectories *) text {* \lsthaskell{Thy/code_examples/Classes.hs} - \noindent (we have left out all other modules). - \noindent The whole code in SML with explicit dictionary passing: *} -code_gen example (*<*)in SML(*>*)in SML file "code_examples/classes.ML" +code_gen example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML" text {* \lstsml{Thy/code_examples/classes.ML} diff -r f1ba12c117ec -r 48494ccfabaf doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Tue Jul 24 15:20:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Tue Jul 24 15:21:54 2007 +0200 @@ -1,61 +1,59 @@ module Classes where { -import qualified Integer; -import qualified Nat; + +data Nat = Zero_nat | Suc Nat; + +data Bit = B0 | B1; + +nat_aux :: Integer -> Nat -> Nat; +nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n)); + +nat :: Integer -> Nat; +nat i = nat_aux i Zero_nat; class Semigroup a where { mult :: a -> a -> a; }; -class (Classes.Semigroup a) => Monoidl a where { +class (Semigroup a) => Monoidl a where { neutral :: a; }; -class (Classes.Monoidl a) => Group a where { +class (Monoidl a) => Group a where { inverse :: a -> a; }; -inverse_int :: Integer.Inta -> Integer.Inta; -inverse_int i = Integer.uminus_int i; +inverse_int :: Integer -> Integer; +inverse_int i = negate i; -neutral_int :: Integer.Inta; -neutral_int = Integer.Number_of_int Integer.Pls; +neutral_int :: Integer; +neutral_int = 0; -mult_int :: Integer.Inta -> Integer.Inta -> Integer.Inta; -mult_int i j = Integer.plus_int i j; +mult_int :: Integer -> Integer -> Integer; +mult_int i j = i + j; -instance Classes.Semigroup Integer.Inta where { - mult = Classes.mult_int; +instance Semigroup Integer where { + mult = mult_int; }; -instance Classes.Monoidl Integer.Inta where { - neutral = Classes.neutral_int; -}; - -instance Classes.Group Integer.Inta where { - inverse = Classes.inverse_int; +instance Monoidl Integer where { + neutral = neutral_int; }; -pow_nat :: (Classes.Monoidl b) => Nat.Nat -> b -> b; -pow_nat (Nat.Suc n) x = Classes.mult x (Classes.pow_nat n x); -pow_nat Nat.Zero_nat x = Classes.neutral; +instance Group Integer where { + inverse = inverse_int; +}; -pow_int :: (Classes.Group a) => Integer.Inta -> a -> a; -pow_int k x = - (if Integer.less_eq_int (Integer.Number_of_int Integer.Pls) k - then Classes.pow_nat (Integer.nat k) x - else Classes.inverse - (Classes.pow_nat (Integer.nat (Integer.uminus_int k)) x)); +pow_nat :: (Group b) => Nat -> b -> b; +pow_nat (Suc n) x = mult x (pow_nat n x); +pow_nat Zero_nat x = neutral; -example :: Integer.Inta; -example = - Classes.pow_int - (Integer.Number_of_int - (Integer.Bit - (Integer.Bit - (Integer.Bit (Integer.Bit Integer.Pls Integer.B1) Integer.B0) - Integer.B1) - Integer.B0)) - (Integer.Number_of_int (Integer.Bit Integer.Min Integer.B0)); +pow_int :: (Group a) => Integer -> a -> a; +pow_int k x = + (if 0 <= k then pow_nat (nat k) x + else inverse (pow_nat (nat (negate k)) x)); + +example :: Integer; +example = pow_int 10 (-2); } diff -r f1ba12c117ec -r 48494ccfabaf doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Jul 24 15:20:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Tue Jul 24 15:21:54 2007 +0200 @@ -1,141 +1,53 @@ -structure ROOT = -struct - -structure Nat = +structure Classes = struct datatype nat = Zero_nat | Suc of nat; -end; (*struct Nat*) - -structure Integer = -struct - datatype bit = B0 | B1; -datatype int = Pls | Min | Bit of int * bit | Number_of_int of int; - -fun pred (Bit (k, B0)) = Bit (pred k, B1) - | pred (Bit (k, B1)) = Bit (k, B0) - | pred Min = Bit (Min, B0) - | pred Pls = Min; - -fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w) - | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0) - | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1) - | uminus_int Min = Bit (Pls, B1) - | uminus_int Pls = Pls; - -fun succ (Bit (k, B0)) = Bit (k, B1) - | succ (Bit (k, B1)) = Bit (succ k, B0) - | succ Min = Pls - | succ Pls = Bit (Pls, B1); - -fun plus_int (Number_of_int v) (Number_of_int w) = - Number_of_int (plus_int v w) - | plus_int k Min = pred k - | plus_int k Pls = k - | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0) - | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1) - | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b) - | plus_int Min k = pred k - | plus_int Pls k = k; - -fun minus_int (Number_of_int v) (Number_of_int w) = - Number_of_int (plus_int v (uminus_int w)) - | minus_int z w = plus_int z (uminus_int w); +fun nat_aux i n = + (if IntInf.<= (i, (0 : IntInf.int)) then n + else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n)); -fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l - | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2 - | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2 - | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2 - | less_eq_int (Bit (k, v)) Min = less_eq_int k Min - | less_eq_int (Bit (k, B1)) Pls = less_int k Pls - | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls - | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k - | less_eq_int Min (Bit (k, B0)) = less_int Min k - | less_eq_int Min Min = true - | less_eq_int Min Pls = true - | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k - | less_eq_int Pls Min = false - | less_eq_int Pls Pls = true -and less_int (Number_of_int k) (Number_of_int l) = less_int k l - | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2 - | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2 - | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2 - | less_int (Bit (k, B1)) Min = less_int k Min - | less_int (Bit (k, B0)) Min = less_eq_int k Min - | less_int (Bit (k, v)) Pls = less_int k Pls - | less_int Min (Bit (k, v)) = less_int Min k - | less_int Min Min = false - | less_int Min Pls = true - | less_int Pls (Bit (k, B1)) = less_eq_int Pls k - | less_int Pls (Bit (k, B0)) = less_int Pls k - | less_int Pls Min = false - | less_int Pls Pls = false; - -fun nat_aux n i = - (if less_eq_int i (Number_of_int Pls) then n - else nat_aux (Nat.Suc n) - (minus_int i (Number_of_int (Bit (Pls, B1))))); - -fun nat i = nat_aux Nat.Zero_nat i; - -end; (*struct Integer*) - -structure Classes = -struct +fun nat i = nat_aux i Zero_nat; type 'a semigroup = {mult : 'a -> 'a -> 'a}; fun mult (A_:'a semigroup) = #mult A_; type 'a monoidl = - {Classes__monoidl_semigroup : 'a semigroup, neutral : 'a}; -fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_; + {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a}; +fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_; fun neutral (A_:'a monoidl) = #neutral A_; -type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a}; -fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_; +type 'a group = {Classes__monoidl_group : 'a monoidl, inverse : 'a -> 'a}; +fun monoidl_group (A_:'a group) = #Classes__monoidl_group A_; fun inverse (A_:'a group) = #inverse A_; -fun inverse_int i = Integer.uminus_int i; +fun inverse_int i = IntInf.~ i; -val neutral_int : Integer.int = Integer.Number_of_int Integer.Pls; +val neutral_int : IntInf.int = (0 : IntInf.int); -fun mult_int i j = Integer.plus_int i j; +fun mult_int i j = IntInf.+ (i, j); -val semigroup_int = {mult = mult_int} : Integer.int semigroup; +val semigroup_int = {mult = mult_int} : IntInf.int semigroup; val monoidl_int = - {Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} : - Integer.int monoidl; + {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} : + IntInf.int monoidl; val group_int = - {Classes__group_monoidl = monoidl_int, inverse = inverse_int} : - Integer.int group; + {Classes__monoidl_group = monoidl_int, inverse = inverse_int} : + IntInf.int group; -fun pow_nat B_ (Nat.Suc n) x = - mult (monoidl_semigroup B_) x (pow_nat B_ n x) - | pow_nat B_ Nat.Zero_nat x = neutral B_; +fun pow_nat B_ (Suc n) x = + mult ((semigroup_monoidl o monoidl_group) B_) x (pow_nat B_ n x) + | pow_nat B_ Zero_nat x = neutral (monoidl_group B_); fun pow_int A_ k x = - (if Integer.less_eq_int (Integer.Number_of_int Integer.Pls) k - then pow_nat (group_monoidl A_) (Integer.nat k) x - else inverse A_ - (pow_nat (group_monoidl A_) - (Integer.nat (Integer.uminus_int k)) x)); + (if IntInf.<= ((0 : IntInf.int), k) then pow_nat A_ (nat k) x + else inverse A_ (pow_nat A_ (nat (IntInf.~ k)) x)); -val example : Integer.int = - pow_int group_int - (Integer.Number_of_int - (Integer.Bit - (Integer.Bit - (Integer.Bit - (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0), - Integer.B1), - Integer.B0))) - (Integer.Number_of_int (Integer.Bit (Integer.Min, Integer.B0))); +val example : IntInf.int = + pow_int group_int (10 : IntInf.int) (~2 : IntInf.int); end; (*struct Classes*) - -end; (*struct ROOT*) diff -r f1ba12c117ec -r 48494ccfabaf doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Jul 24 15:20:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Jul 24 15:21:54 2007 +0200 @@ -85,7 +85,7 @@ Indeed, type classes not only allow for simple overloading but form a generic calculus, an instance of order-sorted - algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}. + algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}. From a software enigineering point of view, type classes correspond to interfaces in object-oriented languages like Java; @@ -115,7 +115,8 @@ \item instantating those abstract operations by a particular type \item in connection with a ``less ad-hoc'' approach to overloading, - \item with a direct link to the Isabelle module system (aka locales). + \item with a direct link to the Isabelle module system + (aka locales \cite{kammueller-locales}). \end{enumerate} \noindent Isar type classes also directly support code generation @@ -124,12 +125,12 @@ This tutorial demonstrates common elements of structured specifications and abstract reasoning with type classes by the algebraic hierarchy of semigroups, monoids and groups. Our background theory is that of - Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some + Isabelle/HOL \cite{isa-tutorial}, for which some familiarity is assumed. Here we merely present the look-and-feel for end users. Internally, those are mapped to more primitive Isabelle concepts. - See \cite{haftmann_wenzel2006classes} for more detail.% + See \cite{Haftmann-Wenzel:2006:classes} for more detail.% \end{isamarkuptext}% \isamarkuptrue% % @@ -662,6 +663,35 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Derived definitions% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Isabelle locales support a concept of local definitions + in locales:% +\end{isamarkuptext}% +\isamarkuptrue% +\ \ \ \ \isacommand{fun}\isamarkupfalse% +\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline +\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}% +\begin{isamarkuptext}% +\noindent If the locale \isa{group} is also a class, this local + definition is propagated onto a global definition of + \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}} + with corresponding theorems + + \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline% +pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}. + + \noindent As you can see from this example, for local + definitions you may use any specification tool + which works together with locales (e.g. \cite{krauss2006}).% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Further issues% } \isamarkuptrue% @@ -679,12 +709,12 @@ takes this into account. Concerning target languages lacking type classes (e.g.~SML), type classes are implemented by explicit dictionary construction. - As example, the natural power function on groups:% + For example, lets go back to the power function:% \end{isamarkuptext}% \isamarkuptrue% \ \ \ \ \isacommand{fun}\isamarkupfalse% \isanewline -\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline \isanewline @@ -704,17 +734,15 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ example\ \isakeyword{in}\ Haskell\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}% +\ example\ \isakeyword{in}\ Haskell\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}% \begin{isamarkuptext}% \lsthaskell{Thy/code_examples/Classes.hs} - \noindent (we have left out all other modules). - \noindent The whole code in SML with explicit dictionary passing:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ example\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}% +\ example\ \isakeyword{in}\ SML\ \isakeyword{to}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/code_examples/classes.ML}% \end{isamarkuptext}% diff -r f1ba12c117ec -r 48494ccfabaf doc-src/IsarAdvanced/Classes/classes.bib --- a/doc-src/IsarAdvanced/Classes/classes.bib Tue Jul 24 15:20:53 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,211 +0,0 @@ - -@InProceedings{Ballarin:2004, - author = {Clemens Ballarin}, - title = {Locales and Locale Expressions in {Isabelle/Isar}}, - booktitle = {Types for Proofs and Programs (TYPES 2003)}, - year = 2004, - editor = {Stefano Berardi and others}, - series = {LNCS 3085} -} - -@InProceedings{Ballarin:2006, - author = {Clemens Ballarin}, - title = {Interpretation of Locales in {Isabelle}: Theories and Proof Contexts}, - booktitle = {Mathematical Knowledge Management (MKM 2006)}, - year = 2006, - editor = {J.M. Borwein and W.M. Farmer}, - series = {LNAI 4108} -} - -@InProceedings{Berghofer-Nipkow:2000, - author = {Stefan Berghofer and Tobias Nipkow}, - title = {Proof terms for simply typed higher order logic}, - booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} 2000)}, - editor = {J. Harrison and M. Aagaard}, - series = {LNCS 1869}, - year = 2000 -} - -@Manual{Coq-Manual:2006, - title = {The {Coq} Proof Assistant Reference Manual, version 8}, - author = {B. Barras and others}, - organization = {INRIA}, - year = 2006 -} - -@Article{Courant:2006, - author = {Judica{\"e}l Courant}, - title = {{$\mathcal{MC}_2$: A Module Calculus for Pure Type Systems}}, - journal = {The Journal of Functional Programming}, - year = 2006, - note = {To appear}, - abstract = {Several proof-assistants rely on the very formal basis - of Pure Type Systems (PTS) as their foundations. We are concerned - with the issues involved in the development of large proofs in - these provers such as namespace management, development of - reusable proof libraries and separate verification. Although - implementations offer many features to address them, few - theoretical foundations have been laid for them up to now. This is - a problem as features dealing with modularity may have harmful, - unsuspected effects on the reliability or usability of an - implementation. - - In this paper, we propose an extension of Pure Type Systems with a - module system, MC2, adapted from SML-like module systems for - programming languages. This system gives a theoretical framework - addressing the issues mentioned above in a quite uniform way. It - is intended to be a theoretical foundation for the module systems - of proof-assistants such as Coq or Agda. We show how reliability - and usability can be formalized as metatheoretical properties and - prove they hold for MC2.} -} - -@PhdThesis{Jacek:2004, - author = {Jacek Chrz\c{a}szcz}, - title = {Modules in type theory with generative definitions}, - school = {Universit{\'e} Paris-Sud}, - year = {2004}, -} - -@InProceedings{Kamm-et-al:1999, - author = {Florian Kamm{\"u}ller and Markus Wenzel and - Lawrence C. Paulson}, - title = {Locales: A Sectioning Concept for {Isabelle}}, - booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} '99)}, - editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and - Paulin, C. and Thery, L.}, - series = {LNCS 1690}, - year = 1999 -} - -@InProceedings{Nipkow-Prehofer:1993, - author = {T. Nipkow and C. Prehofer}, - title = {Type checking type classes}, - booktitle = {ACM Symp.\ Principles of Programming Languages}, - year = 1993 -} - -@Book{Nipkow-et-al:2002:tutorial, - author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, - title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, - series = {LNCS 2283}, - year = 2002 -} - -@InCollection{Nipkow:1993, - author = {T. Nipkow}, - title = {Order-Sorted Polymorphism in {Isabelle}}, - booktitle = {Logical Environments}, - publisher = {Cambridge University Press}, - year = 1993, - editor = {G. Huet and G. Plotkin} -} - -@InProceedings{Nipkow:2002, - author = {Tobias Nipkow}, - title = {Structured Proofs in {Isar/HOL}}, - booktitle = {Types for Proofs and Programs (TYPES 2002)}, - year = 2003, - editor = {H. Geuvers and F. Wiedijk}, - series = {LNCS 2646} -} - -@InCollection{Paulson:1990, - author = {L. C. Paulson}, - title = {Isabelle: the next 700 theorem provers}, - booktitle = {Logic and Computer Science}, - publisher = {Academic Press}, - year = 1990, - editor = {P. Odifreddi} -} - -@BOOK{Pierce:TypeSystems, - AUTHOR = {B.C. Pierce}, - TITLE = {Types and Programming Languages}, - PUBLISHER = {MIT Press}, - YEAR = 2002, - PLCLUB = {Yes}, - BCP = {Yes}, - KEYS = {books}, - HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/tapl}, - ERRATA = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt} -} - -@Book{Schmidt-Schauss:1989, - author = {Manfred Schmidt-Schau{\ss}}, - title = {Computational Aspects of an Order-Sorted Logic with Term Declarations}, - series = {LNAI 395}, - year = 1989 -} - -@InProceedings{Wenzel:1997, - author = {M. Wenzel}, - title = {Type Classes and Overloading in Higher-Order Logic}, - booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} '97)}, - editor = {Elsa L. Gunter and Amy Felty}, - series = {LNCS 1275}, - year = 1997} - -@article{hall96type, - author = "Cordelia Hall and Kevin Hammond and Peyton Jones, S. and Philip Wadler", - title = "Type Classes in {Haskell}", - journal = "ACM Transactions on Programming Languages and Systems", - volume = "18", - number = "2", - publisher = "ACM Press", - year = "1996" -} - -@inproceedings{hindleymilner, - author = {L. Damas and H. Milner}, - title = {Principal type schemes for functional programs}, - booktitle = {ACM Symp. Principles of Programming Languages}, - year = 1982 -} - -@manual{isabelle-axclass, - author = {Markus Wenzel}, - title = {Using Axiomatic Type Classes in {I}sabelle}, - institution = {TU Munich}, - year = 2005, - note = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}} - -@InProceedings{krauss:2006:functions, - author = {A. Krauss}, - title = {Partial Recursive Functions in Higher-Order Logic}, - booktitle = {Int. Joint Conference on Automated Reasoning (IJCAR 2006)}, - year = 2006, - editor = {Ulrich Furbach and Natarajan Shankar}, - series = {LNCS} -} - -@inproceedings{peterson93implementing, - author = "J. Peterson and Peyton Jones, S.", - title = "Implementing Type Classes", - booktitle = "{SIGPLAN} Conference on Programming Language Design and Implementation", - year = 1993 -} - -@inproceedings{wadler89how, - author = {P. Wadler and S. Blott}, - title = {How to make ad-hoc polymorphism less ad-hoc}, - booktitle = {ACM Symp.\ Principles of Programming Languages}, - year = 1989 -} - -@misc{jones97type, - author = "S. Jones and M. Jones and E. Meijer", - title = "Type classes: an exploration of the design space", - text = "Simon Peyton Jones, Mark Jones, and Erik Meijer. Type classes: an exploration - of the design space. In Haskell Workshop, June 1997.", - year = "1997", - url = "citeseer.ist.psu.edu/peytonjones97type.html" -} - -@article{haftmann_wenzel2006classes, - author = "Florian Haftmann and Makarius Wenzel", - title = "Constructive Type Classes in Isabelle", - year = 2006, - note = {To appear} -} - diff -r f1ba12c117ec -r 48494ccfabaf doc-src/IsarAdvanced/Classes/classes.tex --- a/doc-src/IsarAdvanced/Classes/classes.tex Tue Jul 24 15:20:53 2007 +0200 +++ b/doc-src/IsarAdvanced/Classes/classes.tex Tue Jul 24 15:21:54 2007 +0200 @@ -79,7 +79,7 @@ \begingroup %\tocentry{\bibname} \bibliographystyle{plain} \small\raggedright\frenchspacing -\bibliography{../../manual,classes} +\bibliography{../../manual} \endgroup \end{document} diff -r f1ba12c117ec -r 48494ccfabaf doc-src/manual.bib --- a/doc-src/manual.bib Tue Jul 24 15:20:53 2007 +0200 +++ b/doc-src/manual.bib Tue Jul 24 15:21:54 2007 +0200 @@ -441,6 +441,13 @@ %H +@InProceedings{Haftmann-Wenzel:2006:classes, + author = {Florian Haftmann and Makarius Wenzel}, + title = {Constructive Type Classes in {Isabelle}}, + year = 2006, + note = {To appear} +} + @manual{isabelle-classes, author = {Florian Haftmann}, title = {Haskell-style type classes with {Isabelle}/{Isar}}, @@ -803,6 +810,13 @@ year = 1995, pages = {201-224}} +@InProceedings{Nipkow-Prehofer:1993, + author = {T. Nipkow and C. Prehofer}, + title = {Type checking type classes}, + booktitle = {ACM Symp.\ Principles of Programming Languages}, + year = 1993 +} + @Book{isa-tutorial, author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic}, @@ -1231,6 +1245,13 @@ %W +@inproceedings{wadler89how, + author = {P. Wadler and S. Blott}, + title = {How to make ad-hoc polymorphism less ad-hoc}, + booktitle = {ACM Symp.\ Principles of Programming Languages}, + year = 1989 +} + @Misc{x-symbol, author = {Christoph Wedler}, title = {Emacs package ``{X-Symbol}''}, @@ -1531,6 +1552,6 @@ year = 2006} @unpublished{classes_modules, - title = {ML Modules and Haskell Type Classes: A Constructive Comparison}, + title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison}, author = {Stefan Wehr et. al.} }