Research/Study in Logics, Types, Rewriting, & Applications
The ULTRA group (Useful Logics, Types, Rewriting, and Applications) at Heriot-Watt University in Edinburgh is seeking active and energetic candidates for the following positions: * 2 postdoctoral research positions, 6 months each (extendable depending on performance and funding), starting 1 October 2000 (possibly negotiable) * 1 postgrad student position Preference will be given to candidates with strong backgrounds in one or more of the following areas: * Type inference (i.e., searching for types given an untyped program) and the use of types for program analysis. Expertise in intersection/union types is especially useful, but not necessary. * Equational reasoning for programming language semantics, including imperative features (I/O, assignments, etc.). * Logics (both classical and constructive), type theories, rewriting systems (including lambda calculus), and their interaction in the Proofs-as-Programs/Propositions-as-Types correspondence (a.k.a. the Curry/Howard/de Bruijn correspondence). * Notions of binding, reference, and substitution, including such areas as explicit substitutions, generalized notions of reduction, and mechanisms for supporting type definitions in typed calculi. In all of these areas, there are opportunities both for research in theoretical foundations (e.g., proving termination, confluence, subject reduction, extensions to polymorphic types, etc.) and practical implementations aimed both at programming languages and theorem provers. The ULTRA group does research in the design, implementation, and applications of systems of logic, types, and rewriting. The group regularly organizes international events both at Heriot-Watt and abroad. The group also has strong international collaborations (in particular with the AUTOMATH and Type Theory group in Eindhoven (NL) and the Church Project (USA)) and regularly brings high-level researchers to visit Heriot-Watt. Further information about the ULTRA group can be found at http://www.cee.hw.ac.uk/ultra/>. Interested candidates should send the following: 1. Curriculum vitae. 2. Three letters of recommendation sent to us directly by your references. 3. A two-page description of how your research fits the goals of the ULTRA group. This material should be sent to either Prof. Fairouz Kamareddine or Dr. Joe Wells at one of these addresses: Postal: Heriot-Watt University Dept. of Computing & Electrical Eng. Riccarton, EDINBURGH, EH14 4AS Scotland, UK E-mail: [EMAIL PROTECTED], [EMAIL PROTECTED] Fax: +44 131 451 3327 Further information can be obtained by contacting either Prof. Kamareddine or Dr. Wells.
Re: [ANNOUNCE] HDoc: a "javadoc for Haskell"
Armin, Is HDoc also designed to work with the February 2000 version of Hugs98? Will it work under Linux and MacOS as well as under Win 32 (including Windows 2000)? --Benjamin L. Russell [EMAIL PROTECTED] [EMAIL PROTECTED] On Tue, 8 Aug 2000 20:25:08 +0200 (CEST) Armin Groesslinger <[EMAIL PROTECTED]> wrote: > Hello, > > I have written a small program, HDoc, which can generate > HTML documents from specially annoted Haskell sources; > currently it is possible to document functions, data > types, > classes and instances. The resulting documents are cross > linked and - IMHO - they look pretty nice. So, HDoc > does pretty the same job as javadoc does for Java. > > Currently, _all_ the information is taken from special > comments, i.e. the Haskell code is simply ignored (I > found that it is very difficult (compared to Java) to > extract the necessary information from Haskell code. > > Here's an example of what the special comments > for a function can look like (I admit, it looks a bit > like > javadoc...) > > {--- > @fun square :: Integer -> Integer ! Squares an > integer. > The number is multiplied by itself and the result is > returned. > > @param x :: Integer! the number to be squared. > @return res :: Integer ! the input number squared. > -} > square x = x * x > > -- > > HDoc is not complete or ready for daily use; I'm looking > for > some feedback/ideas etc. HDoc runs on Hugs98 and GHC 4.08 > (other compilers may work, but I haven't tried). > > You can get HDoc from its homepage at > http://www.fmi.uni-passau.de/~groessli/hdoc/ > > An example of HDoc's output (for three very simple > modules) can be viewed at > http://www.fmi.uni-passau.de/~groessli/hdoc/examples/simple/docs/ > > > Please note again: HDoc is in a very early stage (it'll > get a re-write soon to reflect some experiences from the > first version). The main reason for announcing HDoc at > this > time is that I definitely need some feedback on how > useful > HDoc is or can eventually be and what concepts it should > follow etc. > > So if you're interested, please give HDoc a try and send > me > your ideas/suggestions/etc. > > I'm looking forward to receiving your comments! > > > Cheers, > > Armin > > > > >
[ANNOUNCE] HDoc: a "javadoc for Haskell"
Hello, I have written a small program, HDoc, which can generate HTML documents from specially annoted Haskell sources; currently it is possible to document functions, data types, classes and instances. The resulting documents are cross linked and - IMHO - they look pretty nice. So, HDoc does pretty the same job as javadoc does for Java. Currently, _all_ the information is taken from special comments, i.e. the Haskell code is simply ignored (I found that it is very difficult (compared to Java) to extract the necessary information from Haskell code. Here's an example of what the special comments for a function can look like (I admit, it looks a bit like javadoc...) {--- @fun square :: Integer -> Integer ! Squares an integer. The number is multiplied by itself and the result is returned. @param x :: Integer! the number to be squared. @return res :: Integer ! the input number squared. -} square x = x * x -- HDoc is not complete or ready for daily use; I'm looking for some feedback/ideas etc. HDoc runs on Hugs98 and GHC 4.08 (other compilers may work, but I haven't tried). You can get HDoc from its homepage at http://www.fmi.uni-passau.de/~groessli/hdoc/ An example of HDoc's output (for three very simple modules) can be viewed at http://www.fmi.uni-passau.de/~groessli/hdoc/examples/simple/docs/ Please note again: HDoc is in a very early stage (it'll get a re-write soon to reflect some experiences from the first version). The main reason for announcing HDoc at this time is that I definitely need some feedback on how useful HDoc is or can eventually be and what concepts it should follow etc. So if you're interested, please give HDoc a try and send me your ideas/suggestions/etc. I'm looking forward to receiving your comments! Cheers, Armin
RE: unlines: the mystery of the trailing \n
Mark P Jones <[EMAIL PROTECTED]> writes: > > | Here's a Prelude inconsistency that's been irking me once > | in a while for a loong time - today it came up again, so here goes: > | > | unlines ["a","b"] ==> "a\nb\n" > | unwords ["a","b"] ==> "a b" > | > | [... unwords adds space between items, not at the beginning or end; > | unlines puts a newline after each item, including at the end ...] > > I quite like the fact that the definition for unlines gives us laws > like: > > unlines (xs ++ ys) = unlines xs ++ unlines ys > unlines . concat = concat . map unlines > > Of course, the fact that unwords doesn't add a terminating space > means that we don't get quite such nice laws for unwords ... > Hi Mark, yes, those laws would be nice to have too. I guess this shows that treating text as just a list, doesn't give you all the laws you would like. In my case, prepending some lines to a paragraph should ideally have resulted in a bigger paragraph (with no trailing newlines.) Anyway, Pretty gives me the laws I need & is more suitable for the job. No reason to tweak the defn of unlines. --sigbjorn
Re: Haskell and the NGWS Runtime
Tue, 8 Aug 2000 09:17:15 +0200, Erik Meijer <[EMAIL PROTECTED]> pisze: > You hit the nail right on the head wrt to Haskell and .NET. This is > precisely why I am working on Mondrian, which also goes under the name > Haskell#, a pure, lazy functional language that seamlessly fits the .NET > type system. This is what worries me: modifying a bunch of languages to make them incompatible with the rest of the world, locking their users to the .NET platform. Embrace and extend. AFAIK this happened to Java, and is common in C/C++ (using own functions and types instead of ISO/ANSI). -- __("< Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTĘPCZA QRCZAK
Re: unlines: the mystery of the trailing \n
Mon, 7 Aug 2000 17:58:40 -0700, Sigbjorn Finne <[EMAIL PROTECTED]> pisze: > Here's a Prelude inconsistency that's been irking me once > in a while for a loong time - today it came up again, so here goes: > > unlines ["a","b"] ==> "a\nb\n" > unwords ["a","b"] ==> "a b" IMHO it should be that way. Because text files generally do have the final '\n', but lines don't have a final space. Spaces are word separators, '\n' are line terminators. When I map each line of the file, I don't expect dealing with a final empty line. unlines a ++ unlines b = unlines (a++b) > I'd find it a little more useful without the trailing \n > (esp. considering now that putStrLn is std.) writeFile "foo" (unlines listOfLines) Using putStrLn here would be less convenient. -- __("< Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTĘPCZA QRCZAK
Re: Haskell and the NGWS Runtime
Good idea to leave platform wars behind and return to language wars. You hit the nail right on the head wrt to Haskell and .NET. This is precisely why I am working on Mondrian, which also goes under the name Haskell#, a pure, lazy functional language that seamlessly fits the .NET type system. As you can imagine, the type system for such a language will be quite a challenge. The current Mondrian implementation is much like SASL (who remembers that great language) waiting to evolve to Miranda (watching too much Pokemon these days :-) Erik - Original Message - From: "Doug Ransom" <[EMAIL PROTECTED]> To: <[EMAIL PROTECTED]> Sent: Monday, August 07, 2000 7:44 PM Subject: RE: Haskell and the NGWS Runtime Back to the language wars then. It does seem like integration of Haskell and the NGWS is a graunch, largely because Haskell is not OO. Is there anything preventing Haskell from becoming OO and seamlessly fitting into the NGWS? Or from designing a functional language that would be a good fit into the NGWS. A major problem I see is that there is probably a standard set of container classes in NGWS which have a high impedance mismatch with the lists functional languags use for their constructions. Can we ever have functional programming "in the large" given the OO paradigm and NGWS are both here to stay? This can not happen until I can get a language which seamlessly fits into NGWS (or some similar thing on a non-windows platform). -Original Message- From: Antony Courtney [mailto:[EMAIL PROTECTED]] Sent: Sunday, August 06, 2000 3:49 PM To: Jürgen A. Erhard Cc: [EMAIL PROTECTED] Subject: Re: Haskell and the NGWS Runtime "Jürgen A. Erhard" wrote: > > > "Manuel" == Manuel M T Chakravarty <[EMAIL PROTECTED]> writes: > > Manuel> "Erik Meijer" <[EMAIL PROTECTED]> wrote, > >> [...] The lab is *sponsored* by Microsoft, but definitively not *at* > >> Microsoft. I doubt there are any Linux boxes at Microsoft :-) > > Manuel> [...] There have also been reports of Linux boxes in the main > Manuel> company, but the validity of these reports is of course not > > But easy to believe... I mean, wouldn't you take a good look at your > competition? Having spent five years doing Windows and Win32 hacking, and 10+ years doing Unix hacking before that, I can assure you there is little evidence that Microsoft are interested in learning anything whatsoever from Linux or any other Unix work-alike. Rather than re-iterate the argument, I'll simply point interested readers towards the excellent article "Working with Win32: the good, the bad and the ugly" by David G. Korn http://www.usenix.org/publications/login/1997-11/win32.html which mostly reinforces the quote: Those who do not understand Unix are condemned to reinvent it, poorly. -- Henry Spencer Now that I've gotten MY little barb in, can we PLEASE end this tangent on OS wars, and return to our regularly scheduled language wars? :-) Thanks, -Antony (haskell list lurker) -- Antony Courtney [EMAIL PROTECTED] http://www.apocalypse.org/pub/u/antony