src/HOL/MiniML/README.html
changeset 1345 d4e26f632bca
parent 1337 ad834f39d878
child 1519 f999804f11ea
equal deleted inserted replaced
1344:f172a7f14e49 1345:d4e26f632bca
     1 <HTML><HEAD><TITLE>HOL/MiniML/ReadMe</TITLE></HEAD><BODY>
     1 <HTML><HEAD><TITLE>HOL/MiniML/ReadMe</TITLE></HEAD><BODY>
     2 <H2>Type Inference for MiniML</H2>
     2 <H1>Type Inference for MiniML (without <kbd>let</kbd>)</H1>
     3 <H3>(without "let" for the time being)</H3>
       
     4 
     3 
     5 Algorithms W and I are based on
     4 This theory formalizes the basic type inference algorithm underlying all
       
     5 typed functional programming languages. This algorithm is called
       
     6 <kbd>W</kbd>, its more imperative variant is called <kbd>I</kbd>. Both were
       
     7 first described in
     6 <P>
     8 <P>
     7 <KBD>
     9 <KBD>
     8 @article{Milner-Poly,author="Robin Milner",
    10 @article{Milner-Poly,author="Robin Milner",
     9 title="A Theory of Type Polymorphism in Programming",
    11 title="A Theory of Type Polymorphism in Programming",
    10 journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348--375"}
    12 journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348--375"}
    25 @phdthesis{Nazareth-PhD,author={Dieter Nazareth},
    27 @phdthesis{Nazareth-PhD,author={Dieter Nazareth},
    26 title={A Polymorphic Sort System for Axiomatic Specification Languages},
    28 title={A Polymorphic Sort System for Axiomatic Specification Languages},
    27 school={Institut f\"ur Informatik, Technische Universit{\"a}t M{\"u}nchen},
    29 school={Institut f\"ur Informatik, Technische Universit{\"a}t M{\"u}nchen},
    28 year=1995,note={Technical Report {TUM-I9515}}}
    30 year=1995,note={Technical Report {TUM-I9515}}}
    29 </KBD>
    31 </KBD>
    30 </BODY></HTML>
    32 <P>
       
    33 
       
    34 <H2>M.Sc./Diplom Project</H2>
       
    35 
       
    36 Task: extend MiniML with a <kbd>let</kbd>-construct and polymorphic types. We
       
    37 are looking for an enthusiastic student with some basic knowledge of
       
    38 functional programming who is not afraid of logic and proofs.  Sounds
       
    39 interesting? Then contact <A
       
    40 HREF="http://www4.informatik.tu-muenchen.de/~nipkow/">Tobias Nipkow</A> or <A
       
    41 HREF="http://www4.informatik.tu-muenchen.de/~pusch/">Cornelia Pusch</A>.
       
    42 
       
    43 </BODY>
       
    44 </HTML>