February 2008 - Haskell

CFP: Continuation Fest 2008
by oleg＠okmij.org 20 Feb '08

20 Feb '08

Call for Talk Proposals Continuation Fest 2008 April 13, Tokyo, Japan http://logic.cs.tsukuba.ac.jp/~kam/Continuation2008/ Continuations are used, and constantly re-discovered, in web programming, logic, event-based concurrency, linguistics, transactional systems, optimization, program generation and verification. Programming language systems -- including Scheme, OCaml, Ruby, Python, Haskell, Coq -- are (re-)implementing continuations, generators, iterators and related control structures. Continuations are also being studied for their own sake. We call for an informal gathering of people working in all these areas -- language designers, users, and researchers who study or use continuations in academic or practical work or as a hobby. The goal is to exchange ideas, terminology, new results, experience reports, works in progress, open problems, and friendly feedback -- as well as meet each other and strengthen the community. We plan a combination of 7-8 broadly accessible talks and 1-2 invited talks, with plenty of breaks for socializing and informal conversations. An evening event is planned. Participants are invited to submit working notes, source files, and abstracts for distribution to the attendees, but as the workshop has no formal proceedings, contributions may still be submitted for publication elsewhere. We solicit talk proposals, about 2 paragraphs long. The proposal should include the desired talk duration and be emailed to CF2008(a)logic.cs.tsukuba.ac.jp The proposals will be evaluated by the Program Committee, who also would advise the authors on the duration of the talk and on making it as accessible as possible. The topics of interest include, but are not at all limited to: -- descriptions of uses of continuations in program generation, linguistics, proof theory, model checking, -- system demonstrations -- libraries using continuations, such as generators -- verifying programs that use continuations explicitly or implicitly (exceptions, concurrency, backtracking) -- type systems of continuations and their formalizations -- open problems Important dates: March 31, 2008: The deadline for the talk proposals April 13, 2008: The Fest Program committee: Chris Barker (New York) Shiro Kawai (Scheme Arts) Oleg Kiselyov (FNMOC) Chung-chieh Shan (Chair, Rutgers) Taiichi Yuasa (Kyoto) Organizing Committee: Kenichi Asai (Ochanomizu) Yukiyoshi Kameyama (Chair, Tsukuba) Inquiries: CF2008(a)logic.cs.tsukuba.ac.jp

1 0

Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
by Wolfgang Jeltsch 19 Feb '08

19 Feb '08

Am Dienstag, 19. Februar 2008 21:44 schrieben Sie: > * Support of type-level Booleans (Wolfgang?) Attached is just a quickly hacked Boolean module. Nothing very special. I’d be happy if you could prettify this (choose better names, add documentation, etc.). Thanks for any effort. Best wishes, Wolfgang

1 1

Funded PhD studentships at the University Of Kent
by S.J.Thompson 18 Feb '08

18 Feb '08

Funding is available for the following PhD studentships within the TCS group at the University of Kent. Applicants should contact the project supervisor directly for further details. Project Supervisor: Dr Olaf Chitil (O.Chitil(a)kent.ac.uk) Project Title: Tracing Functional Programs with Hat Hat (www.haskell.org/hat) is a sophisticated tool for locating faults in Haskell programs. Hat consists of a trace generation system plus various tools for viewing a trace. The aim of the research project is to improve Hat by both extending it and easing its application in practise: (1) Apply several theoretical results of a recent EPSRC project on tracing in Hat (e.g. algorithmic debugging with functions as finite maps). (2) Integrate the trace generator of Hat into the byte code interpreter of the Glasgow Haskell system (GHC). (3) Enable traced code to call and be called from unmodified non-tracing code, such that Hat can use pre-compiled libraries of GHC. Project Title: The Essence of Transfinite Reductions Project Supervisor: Dr Stefan Kahrs (S.M.Kahrs(a)kent.ac.uk) Infinitary Rewriting is an area of Term Rewriting in which research has studied infinitary terms and infinitary reductions. While the notion of infinitary terms is fairly settled, the existing notions of infinitary reduction leave a lot to be desired - the definitions are suspiciously complicated, the established results less than impressive. Thus, there appears to be a lot of room for improvement. There are different angles that are worth exploring. Firstly, there are several alternative ways to define transfinite reductions. Secondly, one would hope that some of these alternative ways lead to good properties of transfinite reduction. Thirdly, it is not even a priori clear what would constitute such a good property. Project Title: Refactoring Proofs Project Supervisor: Prof Simon Thompson (S.J.Thompson(a)kent.ac.uk) Refactoring allows the programmer to modify the design or structure of a program without changing its behaviour. Recent work in the Functional Programming group at Kent has developed refactoring systems for Haskell 98 (HaRe) and Erlang (Wrangler). Programming and proof have much in common, and indeed under the "propositions as types" analogy, they are different views of the same objects. The aim of this project is to explore how refactoring can be incorporated into proof development systems, and will combine theoretical work, implementation and usability analysis to ensure that the results will be of value to users of proof assistants. The aim of this project is to investigate refactoring for proofs.

1 0

Cfp: 3rd Int'l Workshop on Security and Rewriting Techniques Security (SecReT 2008)
by Santiago Escobar 18 Feb '08

18 Feb '08

******************************************************************** SecReT 2008 3rd International Workshop on Security and Rewriting Techniques http://www.dsic.upv.es/workshops/secret08 Sunday, June 22, 2008, Pittsburgh, USA Affiliated workshop of the 21st IEEE Computer Security Foundations Symposium (CSF) and the 23rd IEEE Symposium on Logic In Computer Science (LICS) IMPORTANT DATES Abstract Submission March 31, 2008 Full Paper Submission April 6, 2008 Acceptance Notification May 12, 2008 Camera Ready May 26, 2008 Workshop June 22, 2008 SCOPE The aim of this workshop is to bring together rewriting researchers and security experts, in order to foster their interaction and develop future collaborations in this area, provide a forum for presenting new ideas and work in progress, and enable newcomers to learn about current activities in this area. The workshop focuses on the use of rewriting techniques in all aspects of security. Specific topics include: authentication, encryption, access control and authorization, protocol verification, specification of policies, intrusion detection, integrity of information, control of information leakage, control of distributed and mobile code, etc. Previous instances of SecRet were held in 2006 (S. Servolo, Venice, Italy), and 2007 (Paris, France). LOCATION SecReT'08 will be held at Carnegie Mellon University in Pittsburgh, Pennsylvania, USA. The workshop is associated with the 21st IEEE Computer Security Foundations Symposium (CSF'08) and the 23rd IEEE Symposium on Logic in Computer Science (LICS'08). SUBMISSION PROCEDURE Submission is web-based via a link available in the main web page. Submissions must be received by April 6, 2008. In addition, a title and abstract must be submitted by March 31, 2008. Submitted papers should be at most 15 pages in the ENTCS style, and should include an abstract and the author's information. See the author's instructions of ENTCS style at http://www.entcs.org. PUBLICATION Accepted papers will be published in a preliminary volume available during the workshop. After the workshop, a final version of the proceedings will be published in the Elsevier series Electronic Notes in Theoretical Computer Science (ENTCS). INVITED SPEAKERS Hubert Comon Cachan, France Jonathan Millen MITRE, USA PROGRAM CO-CHAIRS Daniel Dougherty Worcester Polytechnic Institute, USA Santiago Escobar Technical University of Valencia, Spain PROGRAM COMMITTEE Pierpaolo Degano Pisa, Italy Daniel Dougherty Worcester, USA Santiago Escobar Valencia, Spain Maribel Fernandez King's College London, UK Thomas Genet IRISA Rennes, France Joshua Guttman MITRE, USA Catherine Meadows NRL, USA Monica Nesi L'Aquila, Italy Michael Rusinowitch Lorraine, France Ralf Treinen Paris-7, France ********************************************************************

1 0

Lemmas about type functions
by Louis-Julien Guillemette 15 Feb '08

15 Feb '08

Hi all, I've been using GHC's type families somewhat extensively in my type-preserving compiler (BTW, they work great), and quite often I come across the need to prove lemmas about those functions. As far as I understand there's currently no way to handle such lemmas purely at the type level, and I have to encode them as term-level functions. I wonder if I'm missing something, or otherwise if there are plans to provide some way to do this kind of type-level reasoning. Here's a simple example. I encode (de Bruijn) type contexts as lists of types of this form: (t0, (t1, (... , ()...))) I sometimes concatenate type contexts, and need a lemma stating that appending an empty context leaves it unchanged (ts ++ [] == ts). type family Cat ts0 ts type instance Cat () ts' = ts' type instance Cat (s, ts) ts' = (s, Cat ts ts') That is, I need to coerce: Exp (Cat ts ()) into: Exp ts The way I presently do it is through a term-level function that produces a witness that the two types are equivalent, like this: data Equiv s t where Equiv :: (s ~ t) => Equiv s t cat_nil :: EnvRep ts -> Equiv (Cat ts ()) ts cat_nil R0 = Equiv cat_nil (Rs _ ts_r) = case cat_nil ts_r of Equiv -> Equiv coerce :: EnvRep ts -> Exp (Cat ts ()) -> Exp ts coerce ts_r e = case cat_nil ts_r of Equiv -> e Louis

2 1

Downtime, Sat 2008-02-16 1500-1600 UTC: {darcs, hackage, cvs}.haskell.org
by Ian Lynagh 15 Feb '08

15 Feb '08

Hi all, On Saturday 2008-02-16 (tomorrow), monk, which serves as darcs.haskell.org hackage.haskell.org cvs.haskell.org will go down for maintenance sometime probably between 1500 and 1600 UTC. All going well, the outage should be short. Sorry for any inconcenience caused. Thanks Ian

1 0

LFMTP'08 call for papers
by Andreas Abel 15 Feb '08

15 Feb '08

International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) http://www4.in.tum.de/~lfmtp Pittsburgh, PA, USA, 23 June 2008 Affiliated with Logic in Computer Science (LICS 2008) CALL FOR PAPERS Important dates: --------------------------------------------------------------------- Abstract submission: 14 April 2008 Paper submission: 21 April 2008 Author notification: 19 May 2008 Final version: 2 June 2008 Workshop day: 23 June 2008 --------------------------------------------------------------------- The LFMTP workshop continues the International workshop on Logical Frameworks and Meta-languages (LFM) and the MERLIN workshop on MEchanized Reasoning about Languages with variable BIndingIN. Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation on the one hand and their applications in for example proof-carrying code have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss all aspects of logical frameworks and variable binding. The broad subject areas of LFMTP'08 are: * The automation and implementation of the meta-theory of programming languages and related calculi, particularly work which involves variable binding and fresh name generation. * The theoretical and practical issues concerning the encoding of variable binding and fresh name generation, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Case studies of meta-programming, and the mechanization of the (meta)theory of descriptions of programming languages and other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory are particularly welcome. Topics include, but are not limited to * logical framework design * meta-theoretic analysis * applications and comparative studies * implementation techniques * efficient proof representation and validation * proof-generating decision procedures and theorem provers * proof-carrying code * substructural frameworks * semantic foundations * methods for reasoning about logics * formal digital libraries Program Committee: Andreas Abel (LMU Munich) Peter Dybjer (Chalmers University of Technology) Alberto Momigliano (University of Edinburgh) Brigitte Pientka (McGill University) Randy Pollack (University of Edinburgh) Carsten Schuermann (IT University of Copenhagen) Peter Sewell (University of Cambridge) Aaron Stump (Washington University) Christian Urban (TU Munich) Three categories of papers are solicited: * Category A: Detailed and technical accounts of new research: up to fifteen pages including bibliography. * Category B: Shorter accounts of work in progress and proposed further directions, including discussion papers: up to eight pages including bibliography and appendices. * Category C: System descriptions presenting an implemented tool and its novel features: up to six pages. A demonstration is expected to accompany the presentation. Submission is electronic. Authors are required to submit a paper title and a short abstract of about 100 words before submitting the paper. Papers are to be submitted in postscript or PDF format and must conform to the ENTCS style preferably using LaTeX2e. For further information and submission instructions, see the LFMTP web page: http://www4.in.tum.de/~lfmtp Proceedings are to be published as a volume in the Electronic Notes in Theoretical Computer Science (ENTCS) series and will be available to participants at the workshop. Authors of accepted papers are expected to present their paper at the workshop. The organizers: Andreas Abel Christian Urban Theoretical Computer Science Institute for Computer Science Ludwig-Maximilians-University Munich Technical University of Munich Email: andreas.abel(a)ifi.lmu.de Email: urbanc(a)in.tum.de -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich http://www.tcs.informatik.uni-muenchen.de/~abel/

1 0

Re: [Haskell-cafe] Re: [Haskell] Mailing List Archive: Search Broken?
by Janis Voigtlaender 15 Feb '08

15 Feb '08

apfelmus wrote: > Janis Voigtlaender wrote: > >> when searching through gmane, and selecting a single message with a >> hit, one gets only to see that message without its context thread. At >> least I could not find out a way to switch from the found message to >> the thread in which it occurred. > > > The subject line is a hyperlink that points to the context thread of the > message (which is displayed with frames). ... only in the case of haskell.cafe, but not for haskell.general. (see my response to Calvin Smith on the cafe list) Actually, in the case of haskell.general, it seems to work if and only if the current message is the first one in a thread. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

1 0

Mailing List Archive: Search Broken?
by Janis Voigtlaender 15 Feb '08

15 Feb '08

Hi, it seems that something is wrong with the search on http://www.mail-archive.com/haskell@haskell.org/ Only messages from Nov and Dec 2007 are found, no matter what search phrases and date ranges are given. Worked yesterday and delivered search results over the whole history of the archive. Same for haskell-cafe. Anyone knows what is going on? Thanks, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

2 2

ANNOUNCE: lhs2tex-1.13
by Andres Loeh 14 Feb '08

14 Feb '08

lhs2TeX version 1.13 ==================== We are pleased to announce a new release of lhs2TeX, a preprocessor to generate LaTeX code from literate Haskell sources. lhs2TeX includes the following features: * Highly customized output. * Liberal parser -- no restriction to Haskell 98. * Generate multiple versions of a program or document from a single source. * Active documents: call Haskell to generate parts of the document (useful for papers on Haskell). * A manual explaining all the important aspects of lhs2TeX. Changes (w.r.t. lhs2TeX 1.12) ----------------------------- * Compatible with ghc-6.8.{1,2}. * Compatible with cabal-1.2; traditional configure/make installation should still work. * Uses filepath. * LINE pragmas can be disabled with --no-pragmas. * Fixed comment lexing bugs (--> was considered a Haskell comment, \% was considered a TeX comment) * Added a %subst directive for backquoted operators. Requirements and Download ------------------------- A source distribution is available from http://www.cs.uu.nl/~andres/lhs2tex/ Should work on all major platforms, but has mainly been tested on Linux. Binaries will be made available on request. You need a recent version of GHC (6.8.2 is tested, older versions might work) to build lhs2TeX, and, of course, you need a TeX distribution to make use of lhs2TeX's output. The program includes a configuration that is suitable for use with LaTeX. In theory, there should be no problem to generate code for other TeX flavors, such as plainTeX or ConTeXt. Happy lhs2TeXing, Andres Loeh and Ralf Hinze lhs2TeX(a)andres-loeh.de

1 0