- Haskell - Haskell.org

Haskell alterantives for Isabelle or ACL2
by Brian McBride 14 May '03

14 May '03

This is a newbie question. I'm interested in exploring the use of automatic theorem provers for helping with the formal specification of software systems (in my case semantics of languages and protocols). I've found ACL2 and Isabelle (and a few others) - the former uses Lisp as its meta langauge and the latter SML. For various reasons, some non-technical, I'd rather work in Haskell. Are there any systems similar to ACL2 or Isabelle that I should consider. Are there any alternative Haskell based approaches I should consider. Brian McBride HPLabs, Bristol

5 5

IFL'03 Call for Papers
by Phil Trinder 14 May '03

14 May '03

(Apologies for multiple postings) ============================================================ IFL 2003 15th International Workshop on the IMPLEMENTATION OF FUNCTIONAL LANGUAGES Edinburgh Scotland September 8th - 10th, 2003 http://www.macs.hw.ac.uk/~ifl03 ============================================================= Important dates --------------- Registration deadline: August 1st, 2003 Submission deadline : August 22nd, 2003 Workshop : September 8-10th, 2003 ============================================================= Scope of IFL 2003 ----------------- The aim of the workshop is to bring together researchers and users actively engaged in the implementation and application of functional programming languages to discuss results and new directions of research. The workshop is intended to provide an open forum for researchers who wish to present and discuss new ideas and concepts, work in progress, preliminary results etc. related primarily but not exclusively to the implementation of functional or function-based languages. A not necessarily exhaustive list of topics includes language concepts type checking compilation techniques (abstract) interpretation automatic program generation (abstract) machine architectures array processing concurrent/parallel programming and program execution heap management runtime profiling and performance measurements debugging and tracing verification of functional programs tools and programming techniques Contributions on applications of functional programming, e.g., in teaching, or on theoretical work in any of the above areas are also welcome. This year's workshop is co-located with the 4th International Symposium on Trends in Functional Programming (TFP'03) <http://homepages.inf.ed.ac.uk/stg/workshops/ISTFP/>. Contributions ------------- All attendees are encouraged to submit papers to be published in the draft proceedings and to give presentations at the workshop. Submitted papers must be written in English, conform to the LNCS format (available at: http://www.springer.de/comp/authors/index.html) and not exceed 16 pages. Papers should be submitted by August 22nd as postscript or pdf files using the submission page of the workshop accessible through http://www.macs.hw.ac.uk/~ifl03 After the workshop, a high-quality subset of contributions will be published in the Springer LNCS series. All speakers attending the workshop are invited to submit a paper. Papers for the LNCS proceedings will be refereed according to normal conference standards. Greg Michaelson and Phil Trinder (Organizing Committee Chairs) School of Mathematical and Computer Sciences Heriot-Watt University Edinburgh, EH14 4AS E-mail: {greg,trinder}@macs.hw.ac.uk Teleph: +44 (0)131 451 3435 Depart: +44 (0)131 451 3328 Fasmly: +44 (0)131 451 3327 Intrnt: http://www.macs.hw.ac.uk/~greg http://www.macs.hw.ac.uk/~trinder

1 0

Partial Evaluators / Specialiers in/for Haskell
by Jacques Carette 14 May '03

14 May '03

I am looking for source code for any PE system, preferably written in Haskell for a Haskell-like (sub)language. I am aware of "The Mini-Haskell Partial Evaluator" (see http://www.math.chalmers.se/~rjmh/PECourse/Exercises/PE.html) but it currently does not seem to work with recent version(s) of Haskell [nor does the web version seem to work, even on very simple examples]. I am also aware of the extensive litterature, what I am really in search of is source code with a decent license :-). Best of all would be some 'orphan' PE system where the author would like the system to grow, but does not have the time to do so -- I am looking at adopting... Thanks for any help, Dr. Jacques Carette Computing and Software McMaster University

2 1

RE: Haskell alterantives for Isabelle or ACL2
by Simon Peyton-Jones 14 May '03

14 May '03

John Matthews [johnm(a)cse.ogi.edu] writes: The only thing I could find was the following implementation of a first order logic resolution theorem prover, written in Haskell. I don't know anything about it beyond what is on the web page: http://www.cs.yale.edu/homes/cc392/report.html Now, if Brian wants to *reason* about Haskell programs (rather than program in a theorem prover written in Haskell) then the most suitable choice I know of is to use the HOLCF logic in the Isabelle theorem prover. HOLCF combines LCF and HOL, allowing you to prove properties of cpos, least fixedpoints, etc., but also to reason in HOL about purely logical properties at the same time. However, the LCF term language is quite spartan compared to Haskell. For example, you can define continuous datatypes and match against values using case expressions, but there is no support for defining continuous functions by pattern matching. However, there is support for defining purely logical HOL functions via pattern matching. I also know that one of Tom Melham's students formalized aspects of Haskell in the HOL theorem prover, but I don't know the details. Simon | -----Original Message----- | From: haskell-admin(a)haskell.org [mailto:haskell-admin@haskell.org] On Behalf Of Iavor Diatchki | Sent: 13 May 2003 18:41 | To: Brian McBride | Cc: haskell(a)haskell.org | Subject: Re: Haskell alterantives for Isabelle or ACL2 | | hello, | as far as i know there are no real theorem provers using haskell as a | metalanguage. | there also aren't any text editors that can be programmed in haskell, i | wonder how many people have wanted to program their emacs in haskell :-) | | bye iavor | | Brian McBride wrote: | > This is a newbie question. | > | > I'm interested in exploring the use of automatic theorem provers for | > helping with the formal specification of software systems (in my case | > semantics of languages and protocols). | > | > I've found ACL2 and Isabelle (and a few others) - the former uses Lisp | > as its meta langauge and the latter SML. For various reasons, some | > non-technical, I'd rather work in Haskell. Are there any systems | > similar to ACL2 or Isabelle that I should consider. Are there any | > alternative Haskell based approaches I should consider. | > | > Brian McBride | > HPLabs, Bristol | > | > _______________________________________________ | > Haskell mailing list | > Haskell(a)haskell.org | > http://www.haskell.org/mailman/listinfo/haskell | > | | | _______________________________________________ | Haskell mailing list | Haskell(a)haskell.org | http://www.haskell.org/mailman/listinfo/haskell

1 0

RE: HCaAR - haskell.org Website Design
by Markus.Schnell＠infineon.com 13 May '03

13 May '03

Hi all, the communities report says > Haskell programmers are not graphic designers. Just about anyone could make > haskell.org look nicer and more professional. Actually, I think it's very good as it is. I can read it from nearly anywhere with any browser: I like that very much. Other views? Markus

2 1

Research Job: Compositional Reasoning & Analysis for Software Systems @ Heriot-Watt U., Scotland, UK
by Joe Wells 13 May '03

13 May '03

Research Position Useful Logics, Types, Rewriting, and their Automation (ULTRA) Group Computer Science Department School of Mathematical and Computer Sciences Heriot-Watt University Edinburgh, Scotland, UK The HTML version of this job posting can be found at: http://www.macs.hw.ac.uk/~jbw/position-ad.html Description of the Position A research position is available working on modular reasoning and compositional analysis for software at Heriot-Watt University working with Joe Wells. The position is in the ULTRA (Useful Logics, Types, Rewriting, and their Automation) group in the Computer Science Department in the School of Mathematical and Computer Sciences at Heriot-Watt University in Edinburgh, the capital of Scotland. The position involves close collaboration with both the EC-funded DART (Dynamic Assembly, Reconfiguration, and Type-checking) project (members: Genova Univ., Heriot-Watt Univ., Imperial Coll., and Torino Univ.) and the EC, EPSRC, NATO, and NSF-funded Church Project (members: Boston Coll., Boston Univ., Heriot-Watt Univ., Wellesley Coll., etc.). It will be helpful if the researcher is competent in 1 or more of the following knowledge areas which are likely to be used in the project. * Formal calculi for reasoning about the meaning of computer systems (including computer programs), especially those with aspects of (a) modules, linking, and loading, (b) concurrency, (c) mobility, (d) staged compilation, (e) resource usage, (f) classes and objects, etc. * Analysis of systems represented in formal calculi. * Constraint solving and unification. * Type systems, especially those with intersection and union types. * Programming languages used for any of the above. The duration of the position is from 6 months to 1.5 years, depending on the circumstances of the researcher, with extensions possible depending on salary, experience, performance, and funding. Applications to spend a shorter period (e.g., the sabbatical leave of an established academic) will be considered. The initial salary will be commensurate with qualifications and experience in the range from 20311 GBP to 27339 GBP per year. The position is available as soon as 2003-07-16 with the ideal start date being 2003-08-01. It is preferred that before starting the researcher will have completed a Ph.D. in a relevant discipline within Computer Science. Very good Ph.D. students elsewhere who want to spend part of their studies visiting Heriot-Watt will be considered. Applicants from outside the European Economic Area (EEA) will be considered. The researcher will probably collaborate on 1 or more of the following activities. The specific activities will be matched to the strengths of the researcher. * Designing new type systems for compositional (modular) analysis of systems that may involve one or more aspects of concurrency, mobility, modularity, objects, run-time code generation, etc. * Designing analysis algorithms for the new type systems. * Designing theories (e.g., "calculi") for reasoning about the meaning of dynamic software assembly, i.e., doing in a non-traditional order one or more of type checking, code generation, linking, loading, etc. * Making software systems incorporating the new type systems, algorithms, and calculi. * Writing scientific reports on the work done. Contact Information Informal inquiries should be directed to Joe Wells at: web: http://www.macs.hw.ac.uk/~jbw/ e-mail: jbw(a)macs.hw.ac.uk fax: +44 131 449 3834 Formal applications should be directed to the Heriot-Watt Personnel Office at: web: http://www.hw.ac.uk/personnel/ e-mail: personnel(a)hw.ac.uk (responses will usually be by paper mail, telephone, or fax) voice mail: +44 131 451 3475 fax: +44 131 451 3475 minicom: +44 131 451 8212 post: The Personnel Office Lord Balerno Building Heriot-Watt University EDINBURGH EH14 4AS GREAT BRITAIN Applying for the Position Please use the reference code 59/03/L to help prevent your application from getting mixed up. Please convert Microsoft Word documents to a public, standard, and non-proprietary format. The best format is PDF, because some of our staff will encounter difficulties with HTML or PostScript. To formally apply for this position, please do as many as possible of the items in the following list by 2003-06-13. The first 2 are absolutely necessary and the 3rd is quite important. If you expect trouble meeting the deadline, please ask Joe Wells what to do. * Cause 3 reference letters to be sent. (If someone tells you the letters are not needed yet or that less than 3 are needed, this is a mistake. We want to see the letters before choosing who to interview.) * Send the following yourself: + your complete curriculum vitae, and + contact details for the people writing your reference letters. * Get the Heriot-Watt Personnel Office to send you an "application pack". (This contains an application form, an equal opportunities monitoring form, information for applicants with disabilities, and some additional information about Heriot-Watt and the position.) Fill out and return the application form and the equal opportunities monitoring form. If your curriculum vitae is well constructed, then some information requested will be redundant, so just write "see c.v." in those blanks, but please return the application form anyway. * Optionally, also send either of the following: + a brief statement about why your research accomplishments and interests are a good match for the position, and + up to 3 relevant publications of yours. * It is helpful to inform Joe Wells that you are applying so that he knows to ask our personnel office for your application materials. * Anyone who might need a work permit if hired (usually someone who is not a citizen of an EEA country) should also do the following. In addition to possibly being e-mailed or faxed, each letter of reference should also be sent by post on official-looking headed stationery paper and should include details on your whereabouts over the last two years. A work permit application also needs copies of any degree certificates, so it is a good idea to send those also at the same time as you send the rest of your application. Work permit applications can take quite some time for the UK's Home Office to process, so please avoid delays. For your information, the standard solicitation for a reference letter by Heriot-Watt Personnel Office asks the letter writer for details of: * the capacity in which they know the candidate, * the candidate's skills, abilities and performance in relation to the post applied for, * the candidate's employment record including details of the candidate's role and service dates, * their view of the candidate's suitability for the post as a whole, in light of the attached details and their knowledge of the candidate's experience and abilities, * any further relevant information which would assist us in making an appointment.

1 0

ANNOUNCE 0th IOHCC Results - http://iohcc.mgoetze.net/winners.html
by shae＠webwitches.com 12 May '03

12 May '03

The 0th IOHCC Results have been made public! See them at http://iohcc.mgoetze.net/winners.html -- Shae Matijs Erisson - 2 days older than RFC0226 #haskell on irc.freenode.net - We Put the Funk in Funktion 10 PRINT "HELLO" 20 GOTO 10 ; putStr $ fix ("HELLO\n"++)

1 0

ANNOUNCE: HC&A Report (4th edition, May 2003)
by C.Reinke 12 May '03

12 May '03

On behalf of the many contributors, I am happy to announce that the Haskell Communities and Activities Report (4th edition, May 2003) http://www.haskell.org/communities/ is now available from the Haskell Communities home page in several formats: in PDF (with working links and index, yet printable) or, for those who have problems with the PDF, in HTML (using John's secret weapon again) and Postscript. A big thanks here to everyone who contributed information to the report! I hope you will find it as interesting to read as we did. For those of you who haven't heard of these reports before, the first edition of the HC&A Report was released in November 2001, with the goal of helping to improve the communication between the various groups, projects, and individuals working on, with or inspired by Haskell. The idea of these reports is simple: Every six months, a call goes out to all of you on the Haskell mailing list to contribute brief summaries of your own area of work. Many of you respond (eagerly, unprompted, and well in time for the deadline;-) to the call. I then collect all these into a single report and feed it back to this very mailing list. And when we try for the next update in six months, you might want to add your own work, project, research area or group as well. So, please, put that item into your diary now! End of October 2003: target deadline for contributions to the November 2003 edition of the HC&A Report It has become clear that many Haskellers who work on interesting projects no longer have the time to follow the Haskell mailing list closely and may thus miss the calls for contribution. If you are a member or know of such projects, please point them to the current edition, and invite them to "register" with me for a simple email-reminder in the middle of October (and no, you can't register anyone else:). Of course, they'll still have to act on that reminder, but perhaps we can extend our reach this way.. Enjoy (and communicate;-)! Claus Reinke -- Computing Laboratory University of Kent http://www.cs.kent.ac.uk/~cr3/

1 0

RDP'03 - Early registration: May 15!
by Salvador Lucas 12 May '03

12 May '03

[Apologies for multiple copies of this announcement] ****************************************************************** ****************** Call for participation ****************** ****************************************************************** Federated Conference on Rewriting, Deduction and Programming (RDP) including RTA - TLCA - FTP - IFIP WG 1.6 - RULE - UNIF - WFLP - WRS - WST http://www.dsic.upv.es/~rdp03 Valencia, Spain, June 8 - 14, 2003 ------------------------------------------------------------------ We are pleased to announce that the registration and hotel reservation procedures for attending RDP 2003 are open now. Please, follow this link http://www.dsic.upv.es/~rdp03/org/registration_info.html to formalize your registration. A number of rooms have been booked in various hotels near the Conference venue. Please remember that the number of rooms is limited. Requests will be processed on a first come first served basis and will be subject to space availability. Please, follow this link http://www.dsic.upv.es/~rdp03/org/hotel_info.html to eventually formalize your accomodation in one of such hotels. IMPORTANT: The deadline for early registration/accomodation is M a y 1 5, 2 0 0 3 RDP 2003 will take place at the ADEIT building of the "Fundacio Universitat Empresa de Valencia": Plaza Virgen de la Paz, 3 E-46001 Valencia Spain Please, look at the conference WWW site for further travelling information: http://www.dsic.upv.es/~rdp03/org/travelling_info.html The conference will be hosted by the Departamento de Sistemas Informaticos y Computacion (DSIC) at the Universidad Politecnica de Valencia. PARTICIPANTS 14th Int. Conf. on Rewriting Techniques and Applications, RTA'03 6th Int. Conf. on Typed Lambda Calculi and Applications, TLCA'03 4th Int. Workshop on First Order Theorem Proving, FTP'03 IFIP Working Group 1.6 on Term Rewriting 4th Int. Workshop on Rule Based Programming, RULE'03 17th Int. Workshop on Unification, UNIF'03 12th Int. Workshop on Functional and (Constraint) Logic Prog., WFLP'03 3rd Int. Workshop on Red. Strat. in Rewriting and Programming, WRS'03 6th Int. Workshop on Termination, WST'03 DATES RDP : June 8 - 14, 2003 RTA'03 : June 9 - 11 TLCA'03: June 10 - 12 FTP'03 : June 12 - 14 WG 1.6 : June 12 RULE'03: June 9 UNIF'03: June 8 - 9 WFLP'03: June 12 - 13 WRS'03 : June 8 WST'03 : June 13 - 14 ORGANIZERS The ELP group at the Universidad Politecnica de Valencia Officials: Salvador Lucas (chair of the organizing committee) Maria Alpuente (workshops chair) Jose Hernandez (local arrangements) Javier Oliver (secretary) Maria Jose Ramirez (local arrangements chair) German Vidal (publicity chair) CONTACT Salvador Lucas Departamento de Sistemas Informaticos y Computacion (DSIC) Universidad Politecnica de Valencia Camino de Vera, s/n E-46022 Valencia (Spain) phone: + 34 96 387 7353 (73531) fax: + 34 96 387 7359 e-mail: slucas(a)dsic.upv.es URL: http://www.dsic.upv.es/users/elp/slucas.html FURTHER INFORMATION RDP website: http://www.dsic.upv.es/~rdp03 The ELP group: http://www.dsic.upv.es/users/elp/elp.html ******************************************************************

1 0

RE: Additional libraries with GHCi
by Simon Marlow 10 May '03

10 May '03

> My suggestion, therefore, is to add a note to section 3.5.2 > of the GHC user > guide ("Extra Libraries" in the section on GHCi), along the lines of: > > [[ > Additional libraries provided as Haskell Source files (.hs, > .lhs) may be > located by using the "-i" command line option. The directory > name must be > specified without a trailing "/" (or "\") character. > ]] There's a confusing overlap of terminology here: the GHCi documentation is using the term 'library' to mean a library of object code - files called foo.a or foo.lib, whereas you expect 'library' to mean a source code library. The -i option is documented earlier on, in section 3.2.1 ("The search path for finding source files..."). Cheers, Simon

3 2