12 \author{ Paolo Torrini\inst{1} \and
18 \and DFKI Lab Bremen, {\tt \{Christoph.Lueth,Christian.Maeder,Till.Mossakowski\}@dfki.de} }
26   is Isabelle/HOLCF, and the translation is based on a shallow embedding
38 prover may provide useful support for the formal development and the
46 constructor classes, and a syntax for side effects and pseudo-imperative code
55 libraries and efficient automation.  Isabelle/HOLCF \cite{holcf}
64 application designed to support heterogeneous specification and the
65 formal development of programs. It has an interface with Isabelle, and
66 relies on Programatica \cite{Prog04} for parsing and static analysis
73 are devoted to the translation of types, datatypes, classes and function
75 and Sect.~\ref{sec:conclusion} concludes the paper.
90 single-parameter type classes (with some limitations), \emph{case} and
92 recursive data-types and functions. 
94 %lazy lists and \emph{maybe}. 
95 It keeps into account partiality and laziness by
98 is covered only partially; list comprehension, \emph{where} expressions and
99 \emph{let} with patterns are not covered; further built-in types and type
101 not covered at all --- and so for monadic types beyond list and \emph{maybe}.
107 and also consulted the complete static semantics for Haskell 98
117 question is the coincidence of denotational and operational semantics.
135 %Isabelle and AWE. The application is run by a command that takes as arguments
136 %a target logic and an Haskell program, given as a GHC source file. The latter
137 %gets analysed and translated, the result of a successful run being an Isabelle
143 %simpler representation of Isabelle-HOL and Isabelle/HOLCF.  Haskell programs and
145 %formed by a signature and a set of sentences, according to the theoretical
158 functions are total and may not be computable. A non-primitive
164 $\omega$-chains and has a bottom. Isabelle's formalisation, based on
167 generally partial and computability can be expressed in terms of
169 operator, and so, in contrast with Isabelle/HOL, function definition
178 The provision of pcpos, domains and continuous functions by
179 Isabelle/HOLCF eases the translation of Haskell types and functions a
182 dealing with types and classes, one could come to the conclusion that
185 purely lazy language. However, Haskell is a mixed eager and lazy
188 report, ``Predefined Types and Classes'', in section 6.2.  We quote
224 the recursive translation of item $\alpha$ and the renaming according
285 values of type $N$ must be variable (which always matches), and the
326 \>$  and \ \ldots $\\
327 \>$  and \ $\>$\phi'_n \ = \ C'_{n1} \ (lazy~ :: \ w'_1) \ \ldots \ (lazy~ :: \ 
334 (keyword \emph{and}).\footnote {Due to a bug in Isabelle/HOLCF 2005,
347 \section{Translation of Kinds and Type Classes}
349 Type classes in Isabelle and Haskell associate a set of functions to a
356 actually consists of total orders only, and hence it would be
373 and proof obligation may be automatically discharged.
441 \section{Translation of Function Definitions and Terms}
446 \ \mathit{lift} \to \ 'b)$ and $\mathit{flift2} :: \ ('a \Rightarrow \ 'b) \Rightarrow ('a \ \mathit{lift}
457 (\emph{tr} in Isabelle/HOLCF) i.e.  \emph{TT}, \emph{FF} and $\bot$, and
459 Isabelle/HOLCF-defined \emph{If then else fi} and \emph{case} syntax are used
460 to translate conditional and case expressions, respectively.  There are
467 --- and incomplete patterns --- not allowed --- are dealt with by elimination,
470 translated as conditional ones; where expressions and list comprehension are
494   \qquad \quad and \ \ldots \\
495   \qquad \quad and \ f'_n :: \phi'_n \ =
517 compatibility of map and composition.
551 However, the latter makes the Isabelle simplifier loop, and hence needs
600 \section{Conclusion and Related Work}
613 package. It is interesting to note that Haskell functions and product
614 types have to be lifted due to the mixture of eager and lazy evaluation
622 characterisation of monads and on a proof-reuse strategy that actually
627 Miranda \cite{Thompson95,Thompson89,Thompson95b} and Haskell
631 order to deal with features such as currying and polymorphism.
633 --- as for examples, \cite{Huff} translating Haskell to HOLCF, and
636 comparatively more abstract and general.
641 at the object level, allowing explicitly for a clear semantics, and
645 denotational semantics under the assumption that type constructors and
647 constructors and built-in application in Isabelle without loss from
655 %to rely on theory morphisms and on their implementation for Isabelle in the
659 %base translation to Isabelle/HOL which uses AWE and covers state monad types
668 translation of constructor classes and monads, also covering \emph{do}
675 dynamic Hoare and dynamic logic that already have been formalised in
677 Isabelle is part of the Heterogeneous Tool Set Hets and can be
689   Forschungsgemeinschaft} under grants KR \mbox{1191/5-2} and \mbox{KR
691 package and Erwin R. Catesbeiana for pointing out an inconsistency.
734 Here we highlight the main differences the translation to Isabelle/HOLCF and this,
736 HOL).  Function type, product and list are used to translate the corresponding
741 Standard lambda-abstraction ($\lambda $) and function application are used
743 analogous way as in the translation to Isabelle/HOLCF. However, partial functions and
747   recursive} functions (introduced by the keyword \emph{primrec}) and
769 abbreviation for the HOL function, defined in terms of $fst$ and $snd$, which
841   \qquad and \ \ldots \\
842   \qquad and \ \phi'_n \ = \ C'_{n1} \ w'_1 \ \ldots \ w'_h \ | \ \ldots \ | \ 
900   \qquad \qquad \mbox{with \ construction \ and \ proof \ obligations} \\
932 on Isabelle/HOLCF where type have been extended with abstraction ($\Lambda$) and fixed
996 axiomatically --- \emph{eta} (injective) and \emph{bind} (associative, with
997 \emph{eta} as left and right unit) \cite{moggi89}.  Isabelle does not have
1002 signatures and axioms to theorems in ways that preserve operations and
1008 axioms, constants and type declarations. Building a theory morphism from
1010 with $I$, and makes it possible to translate the proofs made in the abstract
1018 monad operations (contained in \emph{MonadOpEta} and \emph{MonadOpBind},
1019 respectively) and the relevant axioms (in \emph{MonadAxms}). To show that a
1116 \emph{Tx} can be built, and then used to instantiate \emph{Monad}. This gives
1117 automatically access to the theorems proven in \emph{Monad} and, modulo
1318   & \qquad \mbox{where} \ f \ \mbox{is \ totally \ defined \ and \ primitive
1322   & \qquad \mbox{where} \ f \ \mbox{is \ totally \ defined \ and \ primitive
1328   & \qquad \mbox{primitive \ recursive \ in \ the \ first \ argument, \ and \ 
1333   & \qquad \mbox{that} \ \tau_1 = \sigma_i(\tau_i) \ \mbox{and \ all \ the \ 

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