45 functional language with lazy evaluation, polymorphic types extended with type
49 In such languages, monadic constructors are extensively used to deal with
53 typed lambda calculus extended with axiomatic type classes. It provides
56 \cite{Paulson94isa,holcf} is Isabelle/HOL conservatively extended with the
65 formal development of programs. It has an interface with Isabelle, and
81 %associated with the translation to Isabelle/HOLCF, in section 7 we show how translation
82 %of monads is carried out with AWE.
90 single-parameter type classes (with some limitations), \emph{case} and
99 \emph{let} with patterns are not covered; further built-in types and type
121 %only total primitive recursive functions. A better semantics with respect to
122 %partiality could be obtained by lifting the type of function values with
125 %hard to be captured with Isabelle-HOL. It also seems hard to overcome the
127 %mentioned for the translation to Isabelle/HOLCF --- with the notable exception of
147 %composition of a signature translation with a translation of all sentences, is
163 \emph{pcpo}) i.e. a set with a partial order which has suprema of
165 axiomatic type classes \cite{Wenzel}, makes it possible to deal with
169 operator, and so, in contrast with Isabelle/HOL, function definition
173 stage, one has to bear with assumptions on function continuity
182 dealing with types and classes, one could come to the conclusion that
242   & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
279 Although a domain with one strict unary constructor, such as $D2$,
338 taken care of. In case of strict arguments (indicated with ! in
361 translated to Isabelle/HOLCF as subclasses of \emph{pcpo} with empty
362 axiomatization.  Methods declarations associated with Haskell classes
363 are translated to independent function declarations with appropriate
378 class methods for $T$. The same is possible with
385 %Not all the problems have been solved with
464 patterns in case expressions is dealt with. Multiple function definitions are
467 --- and incomplete patterns --- not allowed --- are dealt with by elimination,
469 without patterns on the left are dealt with; guarded expressions are
488   \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
497   \qquad \mbox{with} \ f_1::\phi_1, \ldots, f_n::\phi_n \ 
516 We illustrate our translation with a sample proof about the
552 to be replaced with a more suitable simplification theorem:
610 especially with respect to type checking. Isabelle/HOLCF in particular
611 provides with an expressive semantics covering lazy evaluation, as
612 well as with a smart syntax --- also thanks to the \emph{fixrec}
631 order to deal with features such as currying and polymorphism.
639 uses deep embedding to deal with types.  Haskell types are translated
644 case of Isabelle/HOLCF with a translation that follows the lines of a
651 --- however, when we can get it to deal with cases of interest, it
656 %package AWE \cite{AWE}, in order to deal with special cases of monadic
658 % Currently Hets provides with an extension of the
670 \cite{AWE}. However, there are (mainly syntactic) problems (with name
671 clashes) that currently prevent a proper integration with
690   1191/7-2 }. We thank Brian Huffmann for help with the Isabelle/HOLCF
700 to theories in Isabelle/HOL extended with AWE can be defined with the
717   & \quad \mbox{with} \ T \ \mbox{either \ datatype \ or \ defined \ type} \\
744 particularly case expressions with incomplete patterns are not allowed.
752 association with the parameters. This cannot be dealt with automatically in
761 The third conditions is a way to ensure that we do not end up with type
767 $A$ with products of the corresponding values of $f_{1}, \ldots, f_{n}$. The
820    & \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,
859   \qquad \mbox{with} \ f::\phi \ \mbox{not \ occurring \ in} \ t \\
879   \qquad \mbox{with} \ f_1:: (ctx_1 \Rightarrow \tau_{1a} \to \tau_1), 
891   \qquad \qquad \mbox{with \ proof \ obligation}; \\
900   \qquad \qquad \mbox{with \ construction \ and \ proof \ obligations} \\
932 on Isabelle/HOLCF where type have been extended with abstraction ($\Lambda$) and fixed
959   \quad \mbox{with} \ 0 < i \leq k, & \mbox{when} \ data \ TC_1 \ v_{11} \ \ldots \ v_{1m} \ = \ C_{11}::\tau_{11}
985    \quad \mbox{with} \ 0 < i \leq n,
993 \section{Monads with AWE}
995 A monad is a type constructor with two operations that can be specified
996 axiomatically --- \emph{eta} (injective) and \emph{bind} (associative, with
1010 with $I$, and makes it possible to translate the proofs made in the abstract
1017 declaration of a unary type constructor $M$ (in \emph{MonadType}) with the two
1023 obligations associated with specific instances of
1087 monads --- here again, note the difference with overloading. Morphism
1214   K \ = & Eq & \mbox{with \ default \ methods} \ ==, \ /= \\
1260 %  & \qquad \mbox{with} \ {\overline{x}}_1, {\overline{x}}_k \ \subseteq \ 
1311   & \qquad \mbox{with} \ sp_1, \ldots, sp_n \ \mbox{complete \ match} \\
1390    & \qquad \mbox{if} \ p_n = \_, \ \mbox{with} \ p'_1, \ldots,
1397    & \qquad \mbox{with} \ p'_1, \ldots, p'_{n}, q_1, \ldots, q_k \ 

Indexes created Tue Jul 24 14:28:13 CEST 2018