From xhli06 at 163.com Sat Jan 20 09:06:20 2007 From: xhli06 at 163.com (=?gbk?B?wO7Q8erN?=) Date: Sat, 20 Jan 2007 22:06:20 +0800 (CST) Subject: [TYPES] HELP: Need a paper about stable domain. Message-ID: <56141.1403451169301980747.JavaMail.root@bj163app52.163.com> Dear All, I am a newbie of domain theory. Now I want to read a paper published in LNCS 598, a paper on stable domains written by M.Huth, "Cartesian closed categories of domains and the space proj(D)". However, I can not download it from Springer website because the papers before 1997 are secured to our university.Is there anyone who can download the paper and send it to me? Thanks a lot. Xuhui From jas at di.uminho.pt Mon Jan 29 11:59:58 2007 From: jas at di.uminho.pt (=?ISO-8859-1?Q?Jo=E3o?= Saraiva) Date: Mon, 29 Jan 2007 16:59:58 +0000 Subject: [TYPES] ETAPS 2007: Call for Participation Message-ID: <1170089999.3147.104.camel@p109.glmf.di.uminho.pt> ***************************************************************** *** *** *** ETAPS 2007 *** *** March 24 - April 1, 2007 *** *** Braga, Portugal *** *** *** *** http://www.di.uminho.pt/etaps07/ *** *** *** *** CALL FOR PARTICIPATION *** *** *** *** Early Registration Deadline: 12th February, 2007 *** *** *** ***************************************************************** The European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics related to Software Science. It is a confederation of five main conferences, several satellite workshops and other events. ETAPS 2007 is taking place in Braga, Portugal. Braga, capital of the Minho province, is an ancient city in the heart of the green and fertile region known as the Costa Verde. The region is known for its attractiveness in terms of climate, gastronomy, prices, and culture. Braga is known for its barroque churches and splendid 18th century houses. The old city is solemn and antique, but animated with commercial activity and academic life. ============================================================================ 5 Conferences - 18 Satellite Workshops - 3 Tutorials - Tool Demonstrations ============================================================================ ------------------------------------------------------------------------- Main Conferences ------------------------------------------------------------------------- CC 2007: International Conference on Compiler Construction http://cc2007.cs.brown.edu/ ESOP 2007: European Symposium on Programming http://rap.dsi.unifi.it/esop07/ FASE 2007: Fundamental Approaches to Software Engineering http://fase07.di.fc.ul.pt FOSSACS 2007: Foundations of Software Science and Computation Structures http://www2.in.tum.de/~seidl/fossacs07/ TACAS 2007: Tools and Algorithms for the Construction and Analysis of Systems http://www.doc.ic.ac.uk/tacas07/ ----------------------------------------------------------------------- Invited Speakers ----------------------------------------------------------------------- ETAPS 2007: Rance Cleaveland - University of Maryland, USA ETAPS 2007: Bertrand Meyer - ETH Z?rich, Switzerland CC 2007: Don Batory - University of Texas at Austin, USA ESOP 2007: Andrew Pitts - Cambridge University, UK FASE 2007: Jan Bosch - Nokia, Finland FOSSACS 2007: Radha Jagadeesan - DePaul University, USA TACAS 2007: K. Rustan M. Leino - Microsoft Research, USA Further invited speakers are giving talks in the satellite workshops. ----------------------------------------------------------------------- Satellite Workshops ----------------------------------------------------------------------- ACCAT: Applied and Computational Category Theory http://tfs.cs.tu-berlin.de/workshops/accat2007/ AVIS: Int. Workshop on Automated Verification of Infinite-State Systems http://chacs.nrl.navy.mil/AVIS07 Bytecode: Bytecode Semantics, Verification, Analysis and Transformation http://www.sci.univr.it/~spoto/Bytecode07/ COCV: Sixth Workshop on Compiler Optimization Meets Compiler Verification http://pes.cs.tu-berlin.de/cocv2007/ FESCA: Formal Foundations of Embedded Software and Component-Based Software Architectures http://palab.dcs.kcl.ac.uk/fesca/ FinCo: Foundations of Interactive Computation http://www.cs.brown.edu/sites/finco07/ GT-VMT: Int. Workshop on Graph Transformation and Visual Modeling Techniques http://www.cs.le.ac.uk/events/GTVMT07/ HAV: Heap Analysis and Verification http://www.cs.tau.ac.il/~msagiv/hav.html HFL: Hardware design using Functional Languages http://hfl07.hflworkshop.org/ LDTA: Seventh Workshop on Language Descriptions, Tools and Applications http://www.di.uminho.pt/ldta07 MBT: Third Workshop on Model Based Testing http://react.cs.uni-sb.de/mbt2007/ MOMPES: Model-based Methodologies for Pervasive and Embedded Software http://www.di.uminho.pt/mompes OpenCert: Foundations and Techniques for Open Source Software Certification http://opencert.iist.unu.edu/ QAPL: Fifth Workshop on Quantitative Aspects of Programming Languages http://www.cse.yorku.ca/qapl07 SC: Software Composition http://ssel.vub.ac.be/sc2007 SLA++P: Model-driven High-level Programming of Embedded Systems http://web.uni-bamberg.de/wiai/gdi/SLAP07/ TERMGRAPH: Fourth International Workshop on Computing with Terms and Graphs http://www.termgraph.org.uk WITS: Seventh Workshop on Issues in the Theory of Security http://www.dsi.unive.it/IFIPWG1_7/wits2007.html ----------------------------------------------------------------------- Tutorials ----------------------------------------------------------------------- Program Transformation with Stratego/XT Martin Bravenboer (Utrecht University) and Eelco Visser (Delft University of Technology) Beyond the Generators: Practical Techniques for Real-World Software Generation Anthony M. Sloane (Macquarie University) Mobility, Ubiquity, and Security Gilles Barthe (INRIA), David Pichardie (IRISA), David Aspinall (Univ. of Edinburgh), Peter M?ller (ETH Zurich), Lennart Beringer (LMU Munich) and Joe Kiniry (UC Dublin) ----------------------------------------------------------------------- Tool Demonstrations ----------------------------------------------------------------------- Demonstrations of tools presenting advances on the state of the art have been selected and are integrated in the programmes of the main conferences. ----------------------------------------------------------------------- Registration and Contact Details ----------------------------------------------------------------------- For online registration, please visit http://www.di.uminho.pt/etaps07/ and go to menu item "Registration". Contact details are available at the menu item "Contact us". In case of any questions not addressed on the web pages, please email etaps07 at di.uminho.pt. From cdiggins at gmail.com Thu Feb 1 00:52:26 2007 From: cdiggins at gmail.com (Christopher Diggins) Date: Wed, 31 Jan 2007 21:52:26 -0800 Subject: [TYPES] [Request-for-Comments] Cat : A Typed Functional Stack-Based Language Message-ID: I am writing to request comments and criticisms of my paper "Cat: A Typed Functional Stack Based Language". The abstract follows: == "Stack-based application languages, such as Forth and Postscript, traditionally have provided little or no support for functional programming and have lacked a formal static type system. This changed when Manfred von Thun introduced Joy, a functional stack-based language, and Stephan Becher provided an implementation of StrongForth, a dialect of Forth with an informal type system. This paper introduces the semantics and type system for a pure functional programming language which is entirely stack based" == This is my first attempt at a scholarly article, so even what might be considered "obvious" suggestions would still be much appreciated. -- Christopher Diggins http://www.cdiggins.com From Francois.Pottier at inria.fr Thu Feb 1 09:58:51 2007 From: Francois.Pottier at inria.fr (Francois Pottier) Date: Thu, 1 Feb 2007 15:58:51 +0100 Subject: [TYPES] [Request-for-Comments] Cat : A Typed Functional Stack-Based Language In-Reply-To: References: Message-ID: <20070201145850.GC19067@yquem.inria.fr> Hello, On Wed, Jan 31, 2007 at 09:52:26PM -0800, Christopher Diggins wrote: > I am writing to request comments and criticisms of my paper "Cat: A > Typed Functional Stack Based Language". This looks like a nice, elegant type system. But I am curious: what is the motivation for designing a stack-based programming language for use by humans? Doesn't the lack of explicit named variables make programs rather obscure? Or is the language not intended for humans? -- Fran?ois Pottier Francois.Pottier at inria.fr http://cristal.inria.fr/~fpottier/ From pasalic at cs.rice.edu Fri Feb 2 16:51:11 2007 From: pasalic at cs.rice.edu (Emir Pasalic) Date: Fri, 2 Feb 2007 15:51:11 -0600 Subject: [TYPES] GPCE'07 Call for Papers Message-ID: - Apologies for multiple posts - Call for Papers Sixth International Conference on Generative Programming and Component Engineering (GPCE'07) October 1-3, 2007 Salzburg, Austria (co-located with ESWEEK'07) http://www.gpce.org/07 Important Dates: * Submission of abstracts: April 17, 2007 * Submission: April 20, 2007 * Notification: June 10, 2007 * Tutorial and workshop proposals: March 16, 2007 * Tutorial and workshop notification: April 9, 2007 Scope Generative and component approaches are revolutionizing software development similar to how automation and components revolutionized manufacturing. Generative Programming (developing programs that synthesize other programs), Component Engineering (raising the level of modularization and analysis in application design), and Domain-Specific Languages (elevating program specifications to compact domain-specific notations that are easier to write, maintain, and analyze) are key technologies for automating program development. GPCE provides a venue for researchers and practitioners interested in foundational techniques for enhancing the productivity, quality, and time-to-market in software development that stems from deploying standard componentry and automating program generation. In addition to exploring cutting-edge techniques for developing generative and component-based software, our goal is to foster further cross-fertilization between the software engineering research community and the programming languages community. As GPCE is co-located with ESWEEK this year, we also especially encourage papers from the embedded systems community. Submissions 10 pages in SIGPLAN proceedings style (sigplanconf.cls) reporting research results and/or experience related to the topics above (PC chair can advise on appropriateness). We particularly encourage original high-quality reports on applying GPCE technologies to real-world problems, relating ideas and concepts from several topics, or bridging the gap between theory and practice. Please note that in contrast to last year, GPCE 2007 is not using a double-blind reviewing process. Topics GPCE seeks contributions in software engineering and in programming languages related (but not limited) to: * Generative programming o Reuse, meta-programming, partial evaluation, multi-stage and multi-level languages, and step-wise refinement o Semantics, type systems, symbolic computation, linking and explicit substitution, in-lining and macros, templates, and program transformation o Runtime code generation, compilation, active libraries, synthesis from specifications, development methods, generation of non-code artifacts, formal methods, and reflection * Generative techniques for o Product-line architectures o Distributed, real-time and embedded systems o Model-driven development and architecture o Resource bounded/safety critical systems. * Component-based software engineering o Reuse, distributed platforms and middleware, distributed systems, evolution, patterns, development methods, deployment and configuration techniques, and formal methods * Integration of generative and component-based approaches * Domain engineering and domain analysis o Domain-specific languages (DSLs) including visual and UML-based DSLs * Separation of concerns o Aspect-oriented and feature-oriented programming, o Intentional programming and multi-dimensional separation of concerns * Industrial applications * Applications in embedded systems Reports on applications of these techniques to real-world problems are especially encouraged, as are submissions that relate ideas and concepts from several of these topics, or bridge the gap between theory and practice. The program chair is happy to advise on the appropriateness of a particular subject. Submissions must adhere to SIGPLAN's republication policy. Please contact the program chair if you have any questions about how this policy applies to your paper (gpce07 at diku.dk). General Chair * Charles Consel (LABRI/INRIA, Bordeaux) Program Committee Program Chair: * Julia Lawall (DIKU, University of Copenhagen) Program Committee Members: * Edwin Brady (University of St Andrews, UK) * Johan Brichau (Universit? Catholique de Louvain, Belgium) * Rastislav Bodik (UC Berkeley, USA) * Jacques Carette (McMaster University, Canada) * Albert Cheng (University of Houston, USA) * Remi Douence (Ecole des Mines de Nantes-Inria, Lina, France) * Lidia Fuentes (University of M?laga, Spain) * Ian Gorton (Pacific Northwest National Lab) * Jean-Marc Jezequel (IRISA (INRIA & Univ. Rennes 1), France) * Kyo Kang (Pohang University of Science and Technology, Korea) * Siau Cheng Khoo (National University of Singapore, Singapore) * Paul Kelly (Imperial College London, UK) * Anne-Francoise Le Meur (University of Lille 1, France) * Christian Lengauer (University of Passau, Germany) * Sandeep Neema (Vanderbilt University, USA) * Scott Owens (University of Cambridge, UK) * Jens Palsberg (UCLA, USA) * Renaud Pawlak (Rensselaer Polytechnic Institute, USA) * Zoltan Porkolab (Eotvos Lorand University, Hungary) * Robby (Kansas State University, USA) * Peter Sestoft (IT University of Copenhagen, Denmark) * Jeremy Siek (University of Colorado at Boulder, USA) * Tony Sloane (Macquarie University, Australia) * Kevin J. Sullivan (University of Virginia, USA) * Peri Tarr (IBM Thomas J. Watson Research Center, USA) From jeremy.siek at gmail.com Mon Feb 12 01:14:35 2007 From: jeremy.siek at gmail.com (Jeremy Siek) Date: Sun, 11 Feb 2007 23:14:35 -0700 Subject: [TYPES] Gradual Typing for Objects Message-ID: <18C6CEE3-0EEB-4F6A-9F01-1E7DF2234B17@gmail.com> Dear TYPES readers, We're happy to announce a new paper that extends our work on gradual typing (integrating static and dynamic typing). In this paper we show how to provide gradual typing in object-oriented languages with subtyping. http://www.cs.colorado.edu/~siek/gradual-obj.pdf We will present the paper at ECOOP 2007 and would be especially interested in any feedback on the paper before the final submission is due on April 25. Best regards, Jeremy Siek & Walid Taha ______________________________________ Jeremy Siek http://www.cs.colorado.edu/~siek/ Visiting Assistant Professor Department of Computer Science University of Colorado at Boulder From mulhern at gmail.com Fri Feb 9 22:16:37 2007 From: mulhern at gmail.com (mulhern) Date: Fri, 9 Feb 2007 21:16:37 -0600 Subject: [TYPES] Formal proof of type-soundness for references in Coq Message-ID: <54f15b6e0702091916m1d18f8e5n83d2d45c36deabb6@mail.gmail.com> Hi! I've posted a formal proof in Coq of type-soundness for references at http://www.cs.wisc.edu/~mulhern/proofs/type-soundness/references.html. I think it might be interesting to people on the Coq list because it uses the module system. As far as I know, there is no other publicly available formal proof of type-soundness for references available, so it might be interesting to people on the types list as well. -mulhern From crary at cs.cmu.edu Mon Feb 12 11:53:43 2007 From: crary at cs.cmu.edu (Karl Crary) Date: Mon, 12 Feb 2007 11:53:43 -0500 Subject: [TYPES] Formal proof of type-soundness for references in Coq Message-ID: <45D09B97.1020900@cs.cmu.edu> For a formal proof of type soundness for references in Twelf, you can look at our recent POPL paper on mechanizing the metatheory of Standard ML in Twelf. The language we formalize supports references and some other imperative features as well. The proof is publicly available at http://www.cs.cmu.edu/~crary/papers/. -- Karl Crary mulhern wrote: > From: mulhern > Date: February 9, 2007 10:16:37 PM EST > To: types-list at lists.seas.upenn.edu, coq-club at pauillac.inria.fr > Subject: [TYPES] Formal proof of type-soundness for references in Coq > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi! > > I've posted a formal proof in Coq of type-soundness for references at > http://www.cs.wisc.edu/~mulhern/proofs/type-soundness/references.html. > > I think it might be interesting to people on the Coq list because it uses > the module system. > > As far as I know, there is no other publicly available formal proof of > type-soundness for references available, so it might be interesting to > people on the types list as well. > > -mulhern From mulhern at gmail.com Mon Feb 19 21:49:06 2007 From: mulhern at gmail.com (mulhern) Date: Mon, 19 Feb 2007 20:49:06 -0600 Subject: [TYPES] Formal proof of type-soundness for references in Coq In-Reply-To: <54f15b6e0702091916m1d18f8e5n83d2d45c36deabb6@mail.gmail.com> References: <54f15b6e0702091916m1d18f8e5n83d2d45c36deabb6@mail.gmail.com> Message-ID: <54f15b6e0702191849k79aabc76h82767477a4a183ab@mail.gmail.com> Hi! I'ld like to clarify my last statement. Since I'm interested in proof fragments, when I say "proof of type-soundness for references", I mean a proof of type-soundness for a fragmentary language of which every syntactic element, practically, affects the store. I did not mean to include in this category formal proofs of type-soundness for larger languages which may include references. -mulhern On 2/9/07, mulhern wrote: > > Hi! > > I've posted a formal proof in Coq of type-soundness for references at http://www.cs.wisc.edu/~mulhern/proofs/type-soundness/references.html > . > > I think it might be interesting to people on the Coq list because it uses > the module system. > > As far as I know, there is no other publicly available formal proof of > type-soundness for references available, so it might be interesting to > people on the types list as well. > > -mulhern > From pierre.geneves at inria.fr Tue Feb 20 01:53:40 2007 From: pierre.geneves at inria.fr (Pierre Geneves) Date: Tue, 20 Feb 2007 07:53:40 +0100 Subject: [TYPES] XPath typing Message-ID: <200702200654.l1K6s6wM026668@noisetier.inrialpes.fr> Dear TYPES readers, We are happy to announce a new paper on XPath typing. In this paper we prove the decidability of a modal logic with converse for finite trees and present an algorithm using symbolic techniques (BDDs), that we use for the static analysis of XPath in the presence of regular tree types. http://wam.inrialpes.fr/people/geneves/geneves-pldi07.pdf We will present the paper at PLDI'07 and would be especially interested in any feedback on the paper before the final submission due on March 26. Best regards, Pierre Geneves __ Pierre Geneves, Ph.D. +33 (0)4 76 61 52 45. INRIA Rhone-Alpes, 655 avenue de l'Europe, Montbonnot 38334 St Ismier Cedex, France, http://www.pierresoft.com/pierre.geneves From crary at cs.cmu.edu Tue Feb 20 16:01:52 2007 From: crary at cs.cmu.edu (Karl Crary) Date: Tue, 20 Feb 2007 16:01:52 -0500 Subject: [TYPES] Paper announcement: Syntactic Logical Relations for Polymorphic and Recursive Types Message-ID: <45DB61C0.2080404@cs.cmu.edu> I am pleased to announce the availability of the paper "Syntactic Logical Relations for Polymorphic and Recursive Types" at the following URLs: http://www.cs.cmu.edu/~crary/papers/2007/relns.pdf or http://www.cs.cmu.edu/~rwh/papers/polyrecrelns/gdpfs.pdf As always, comments are welcome. Karl Crary (for myself and Robert Harper) ---------- Syntactic Logical Relations for Polymorphic and Recursive Types Karl Crary and Robert Harper The method of logical relations assigns a relational interpretation to types that expresses operational invariants satisfied by all terms of a type. The method is widely used in the study of typed languages, for example to establish contextual equivalences of terms. The chief difficulty in using logical relations is to establish the existence of a suitable relational interpretation. We extend work of Pitts and Birkedal and Harper on constructing relational interpretations of types to polymorphism and recursive types, and apply it to establish parametricity and representation independence properties in a purely operational setting. We argue that, once the existence of a relational interpretation has been established, it is straightforward to use it to establish properties of interest. From Gerard.Boudol at sophia.inria.fr Mon Feb 26 05:01:15 2007 From: Gerard.Boudol at sophia.inria.fr (Gerard Boudol) Date: Mon, 26 Feb 2007 11:01:15 +0100 Subject: [TYPES] logical relations Message-ID: <45E2AFEB.6070901@sophia.inria.fr> Dear all, logical relations are a recurring topic of discussions in the TYPES forum, and some people have sometimes expressed their interest in the memorandum where Gordon Plotkin introduced the terminology (see his post on this list about the Plotkin-Statman conjecture, dated March 29, 1989). With Gordon's agreement, I have scanned my copy of this report, and made it available at http://www-sop.inria.fr/mimosa/Gerard.Boudol/plotkin-memo-SAI-RM-4.pdf I apologize for the poor quality of this document - talking about the appearance: my own copy was not perfect, and scanning it does not improve it. Still I think it is readable. All the best, G?rard From eernst at daimi.au.dk Tue Feb 27 20:20:34 2007 From: eernst at daimi.au.dk (Erik Ernst) Date: Wed, 28 Feb 2007 02:20:34 +0100 Subject: [TYPES] ECOOP 2007 - Call for Student Volunteers Message-ID: ++++++++++++++++++++++ Call for Student Volunteers +++++++++++++++++++++ +++++++++++++++++++++++++ Deadline: April 18th +++++++++++++++++++++++++ ECOOP 2007 is pleased to offer a number of opportunities for Student Volunteers, who are vital to the efficient operation and continued success of ECOOP each year. We strongly encourage students, all around the world, to become involved in the ECOOP Student Volunteer program. In return for helping keep ECOOP running smoothly, you are granted free registration to the conference and (duties, space, and specific requirements permitting) free access to ECOOP plenary sessions, tutorials, workshops, and demos. You should be in Berlin two days before the conference begins to help with preparations and with the conference take-down (Saturday, July 28 - Friday, August 3). Applications should be submitted by April 18, 2007. More information on student volunteering is available at 2007.ecoop.org. We look forward to receiving your application. Dirk Seifert sv at 2007.ecoop.org ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ +++ on behalf of Dirk Seifert, -- Erik Ernst eernst at daimi.au.dk Department of Computer Science, University of Aarhus IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark From royer at ecs.syr.edu Thu Mar 1 15:42:23 2007 From: royer at ecs.syr.edu (James S. Royer) Date: Thu, 1 Mar 2007 15:42:23 -0500 Subject: [TYPES] CFP: 9th Intl. Workshop on Logic & Computational Complexity (LCC'07) Message-ID: CALL FOR PAPERS: 9TH INTL WORKSHOP ON LOGIC AND COMPUTATIONAL COMPLEXITY ------------------------------------------------------------------------ The Logic and Computational Complexity Workshop, LCC'07, will be held 15 July 2007 in Wroclaw, Poland as a satellite workshop of the Logic in Computer Science Conference (LICS'07). SCOPE The workshop aims at furthering an understanding of the fundamental relations between computational complexity and logic. Topics of interest include: * complexity analysis for functional languages * complexity in database theory * complexity in formal methods * complexity-theoretic type systems * computational complexity in higher types * formal methods for complexity analysis of programs * foundations of implicit computational complexity * logical & machine-independent characterizations of complexity classes * logics closely related to complexity classes * proof complexity * semantic approaches to complexity * software that applies LCC ideas FORMAT The program will consist of sessions of contributed papers, invited talks, and software demonstrations. PAPER SUBMISSION The deadline for submissions is April 16, 2007. See the workshop webpage, http://www.cis.syr.edu/~royer/lcc/LCC07/, for submission details. PROGRAM COMMITTEE * Albert Atserias (Polytechnic University of Catalonia) * Ulrich Berger (University of Wales, Swansea) * Andrei Bulatov (Simon Fraser University) * Stephan Kreutzer (Humboldt University of Berlin) * Andrzej Murawski (University of Oxford) * Martin Otto, co-chair (Darmstadt University of Technology) * Kazushige Terui (National Institute of Informatics, Tokyo) * Pawel Urzyczyn, co-chair (University of Warsaw) Important dates 16 April 2007 The submission deadline 12 May 2007 Notification of authors of accepted papers 15 July 2007 LCC Workshop Dates 10-14 August 2007 LICS'07 Dates WWW-pages The LCC home page: http://www.cis.syr.edu/~royer/lcc/ The LICS home page: http://www.lfcs.informatics.ed.ac.uk/lics Contact information James S. Royer Department of Electrial Engineering and Computer Science Syracuse University Syracuse, NY 13244 USA Email: royer at ecs syr edu From cdiggins at gmail.com Sun Mar 18 18:20:45 2007 From: cdiggins at gmail.com (Christopher Diggins) Date: Sun, 18 Mar 2007 15:20:45 -0700 Subject: [TYPES] Request for Comments: Typing Functional Stack-Based Language Message-ID: I'm writing to request comments on a technical report I've written called: Typing Functional Stack-Based Languages. == Abstract Stack-based languages have been in continuous use for approximately four decades, and are still very popular today as intermediate languages. Many of the most well-known stack-based languages (e.g. Forth, Postscript, CIL, JVML) lack support for functional programming at the primitive instruction level. Some notable exceptions are the Joy programming language by Manfred von Thun and the Factor programming language by Slava Pestov. There has also been a recent proposal to add lambda expressions to Forth by Lynas and Stoddart. While functional stack-based languages are gaining popularity, none of these have a static type system. This paper addresses this gap by formally expressing the operational semantics and type system for Cat, a small functional stack-based language. == The rest of the article is available online at http://www.cat-language.com/paper.html. Any comments or suggestions would be greatly appreciated. Thanks again to everyone who responded so generously to my previous request for comments. I've incorporated many of the suggestions into the new paper. - Christopher Diggins From pierre.courtieu at cnam.fr Mon Mar 19 14:32:02 2007 From: pierre.courtieu at cnam.fr (Pierre Courtieu) Date: Mon, 19 Mar 2007 19:32:02 +0100 Subject: [TYPES] CFP: 2nd CFP for RDP Workshop Proof Assistants and Types in Education (PATE) Message-ID: <20070319193202.784db257@centaur.cnam.fr> Second call for paper, the deadline for submission is april 1, 2007. ===================================================================== Call for Papers RDP (RTA 07 + TLCA 07) Workshop PATE Proof Assistants and Types in Education June 25 2007 http://www.rdp07.org/pate.html ===================================================================== This workshop is supported by the EU Types Coordination Action. The purpose of the workshop is to bring together researchers and lecturers interested in applying type theory and proof assistants in teaching. Contributions are solicited in the following subject areas and related topics: - type theory as a language for (teaching) mathematics and programming; - computer assisted informal reasoning; - tools and languages for teaching math and logic; - experience in using proof assistants in class. Submissions and Publication ----------------------------- Authors are invited to submit a paper (max 15 pages) by e-mail to Pierre.Courtieu at cnam.fr by April 1, 2007. Preliminary proceedings will be available at the workshop. Submissions should be in PostScript or PDF format, using ENTCS style files. Important Dates ----------------- Submission deadline: April 1, 2007 Notification: May 15, 2007 Pre-proceedings version due: June 7, 2007 Workshop: June 25, 2007 Programme Committee -------------------- Pierre Courtieu CNAM Paris (Co-Chair) Herman Geuvers Nijmegen (Co-Chair) Hugo Herbelin INRIA Paris Adam Naumowicz Bialystok Claudio Sacerdoti Coen Bologna Pawel Urzyczyn Warsaw From yoriyuki.y at gmail.com Sun Mar 18 12:07:31 2007 From: yoriyuki.y at gmail.com (Yoriyuki Yamagata) Date: Mon, 19 Mar 2007 01:07:31 +0900 Subject: [TYPES] Google Summer of Code Message-ID: The FreeSoftware Initiative Japan(http://www.fsij.org/) is looking for participants of Google Summer of Code(http://code.google.com/soc). Proposed ideas (https://members.fsij.org/trac/soc2007/wiki/Ideas) include developing automatic program verifier, and OCaml related projects. We also accept proposals not directly related to proposed ideas. If your project is selected, you are paid 4500$ from Google. Please read carefully http://code.google.com/soc/tos.html and https://members.fsij.org/trac/soc2007/wiki/Ideas before submitting your proposal. Feel free to ask me if you have a question. Project ideas are: *Automatic program verifier Develop an automatic program verifier with the following features. - Accept any programs in popular programing languages such as C/Java/Ruby and so on. - Produce correct answers for programs in a practical subset of the language. - Produce approximate answers for all programs in the language. - Performance is not a goal. It suffices to demonstrate its capability to small code fragments. However, it must have modular design to future improvement. The project goal is intentionally vague so that we can accept projects using wide range of methodologies. It mainly aims formal verification technique such as source-code model checking or type-based checking, not rule based static checker like lint. Since it is a summer project, improvement of existing checker, or developing core functionality of new checker is suitable. Unlike research projects, our focus is practical benefits to Free Software community. *Improve OCaml internationalization There is no specific requirement. The idea includes - Create a syntax extension which handle Unicode strings and locale-sensitive messages. Create a Unicode-based, locale-sensitive alternative of the standard library. - Create a binding of ICU. Binding must not be bare-bone wrapping. It must be well integrated to OCaml and its programming customs. We accept other ideas as well. * Create Ajax development tool for OCaml Enable seamless Web development by generating JavaScript from OCaml and integrating it to Web framework. * Improve Eclipse plugin of OCaml There is no specific requirement. Please propose suitable improvements. -- yoriyuki From Malcolm.Tyrrell at computing.dcu.ie Wed Mar 28 06:40:53 2007 From: Malcolm.Tyrrell at computing.dcu.ie (Malcolm Tyrrell) Date: Wed, 28 Mar 2007 11:40:53 +0100 Subject: [TYPES] Some questions on logical and prelogical relations Message-ID: <460A4635.5050300@computing.dcu.ie> Hi all. I'm trying gain an intuition for logical and prelogical relations. As they've been discussed on this forum before, perhaps some of you can help. I'll make some observations and then ask some questions. Please point any mistakes in my observations. Thanks for any help, Malcolm OBSERVATIONS: 1. A logical relation is completely defined by its behaviour at the bottom of the type hierarchy. 2. The term "algebraic relation" is used in [1] to describe a weakening of the definition of logical relation. In an algebraic relation, there is some flexibility for how the relation at a function type corresponds to the relations at its domain and codomain types. 3. Given a relation for each base type, there may be many different algebraic relations built over them, one of which is a logical relation. 4. A prelogical relation is an algebraic relation with an additional property about how lambda-abstractions are related. 5. A logical relation is not in general a prelogical relation (since logical relations are not in general preserved by relational composition but prelogical relations always are). QUESTIONS: Q1. Is the notion "algebraic relation" coined by [1], or is it standard? If it's standard, can you suggest a reference? Q2. Is a prelogical relation uniquely defined by its behaviour at base types, or is there still some flexibility, as in the case of algebraic relations? Q3. Given a relation for each base type, must there always exist some prelogical relation defined over the full type heirarchy? REFERENCES: [1] Prelogical Relations, Honsell & Sannella, Information and Computation 178, 2002 ---------------------------- Malcolm Tyrrell, Lero - the Irish Software Engineering Research Centre and School of Computing, Dublin City University, Ireland. From carette at mcmaster.ca Sun Apr 1 09:27:06 2007 From: carette at mcmaster.ca (Jacques Carette) Date: Sun, 01 Apr 2007 09:27:06 -0400 Subject: [TYPES] Co-algebraic semantics of typed lambda-calculus Message-ID: <460FB32A.8080905@mcmaster.ca> I have been able to find some references to the co-algebraic structure (i.e. final semantics) of the untyped lambda-calculus, (work of Honsell and Lenisa, available at http://citeseer.ist.psu.edu/95166.html and http://portal.acm.org/citation.cfm?id=645892.671579&coll=&dl=ACM&CFID=15151515&CFTOKEN=6184618 ), but my search for a typed analogue has not turned up anything. I rather suspect that this has already been done - could someone here provide me with some references? Thanks, Jacques From royer at ecs.syr.edu Wed Apr 11 16:09:01 2007 From: royer at ecs.syr.edu (James S. Royer) Date: Wed, 11 Apr 2007 16:09:01 -0400 Subject: [TYPES] FINAL CFP: 9th Intl Workshop on Logic & Computational Complexity Message-ID: The Logic and Computational Complexity Workshop (LCC'07) will be held on 15 July 2007 in Wroclaw, Poland as a satellite workshop of the Logic in Computer Science Conference (LICS'07). The deadline for submissions is April 16. For submission details, see: http://www.cis.syr.edu/~royer/icc/LCC07/ From urzy at mimuw.edu.pl Fri Apr 20 08:42:03 2007 From: urzy at mimuw.edu.pl (Pawel Urzyczyn) Date: Fri, 20 Apr 2007 14:42:03 +0200 Subject: [TYPES] TLCA List of Open Problems Message-ID: <20070420124203.6D5C514000C9@duch.mimuw.edu.pl> I would like to announce the launch of TLCA List of Open Problems http://tlca.di.unito.it/opltlca/ The List (modeled after the RTA LOOP) aims at collecting unresolved questions (and other relevant information, e.g. about solutions and related results) in the subject areas of the TLCA (Typed Lambda Calculi and Applications) series of conferences. The initial list consists of 21 problems dated from 1958 to 2007. Everyone is invited to submit new problems, solutions and comments to tlca at mimuw.edu.pl or to any of the three editors: Ryu Hasegawa ryu at ms.u-tokyo.ac.jp Luca Paolini paolini at di.unito.it Pawel Urzyczyn urzy at mimuw.edu.pl Best regards, Pawel Urzyczyn From davide at disi.unige.it Tue Apr 24 05:33:34 2007 From: davide at disi.unige.it (Davide Ancona) Date: Tue, 24 Apr 2007 11:33:34 +0200 Subject: [TYPES] available JVM implementations Message-ID: <462DCEEE.3020306@disi.unige.it> Dear all, together with some colleagues involved in a national Italian project (EOS-DUE http://bart.disi.unige.it/EOS2/www_static_pages/index.html) we are working on changes/extensions to the JVM architecture which have a quite strong impact on dynamic typechecking, and since we would like to build a prototype to experiment with, any useful pointer to, and comments on already available JVM implementations is welcome. The ideal implementation we are looking for has not to be necessarily complete, but, rather, well documented and suited to be "easily" extended/modified. Many thanks in advance, Davide Ancona -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Davide Ancona | phone: ++39 (010) 353 6636 DISI | fax: ++39 (010) 353 6699 Universita' di Genova | e-mail: davide at disi.unige.it Via Dodecaneso, 35 | ftp: ftp.disi.unige.it/person/AnconaD 16146 Genova, Italy | www: http://www.disi.unige.it/person/AnconaD ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From angray at beeb.net Sun Apr 29 03:55:14 2007 From: angray at beeb.net (Aaron Gray) Date: Sun, 29 Apr 2007 08:55:14 +0100 Subject: [TYPES] available JVM implementations References: <462DCEEE.3020306@disi.unige.it> Message-ID: <001401c78a33$bcf49820$0200a8c0@AMD2500> There's IBM Jike Research VM. An introductory article :- http://www-128.ibm.com/developerworks/java/library/j-jalapeno/ Jikes is now on SourceForge :- http://jikes.sourceforge.net/ Aaron ----- Original Message ----- From: "Davide Ancona" To: Sent: Tuesday, April 24, 2007 10:33 AM Subject: [TYPES] available JVM implementations >[ The Types Forum, >http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear all, > together with some colleagues involved in a national Italian project > (EOS-DUE http://bart.disi.unige.it/EOS2/www_static_pages/index.html) > we are working on changes/extensions to the JVM architecture which have > a quite strong impact on dynamic typechecking, and since we would like > to build a prototype to experiment with, any useful pointer to, and > comments on already available JVM implementations is welcome. > The ideal implementation we are looking for has not to be necessarily > complete, but, rather, well documented and suited to be "easily" > extended/modified. > > Many thanks in advance, > Davide Ancona > > > -- > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > Davide Ancona | phone: ++39 (010) 353 6636 > DISI | fax: ++39 (010) 353 6699 > Universita' di Genova | e-mail: davide at disi.unige.it > Via Dodecaneso, 35 | ftp: ftp.disi.unige.it/person/AnconaD > 16146 Genova, Italy | www: http://www.disi.unige.it/person/AnconaD > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > > > -- > No virus found in this incoming message. > Checked by AVG Free Edition. > Version: 7.5.463 / Virus Database: 269.6.1/777 - Release Date: 26/04/2007 > 15:23 > From Tim.Sweeney at epicgames.com Mon May 21 15:54:55 2007 From: Tim.Sweeney at epicgames.com (Tim Sweeney) Date: Mon, 21 May 2007 15:54:55 -0400 Subject: [TYPES] Unification within a quantifier prefix Message-ID: <8A4FE0C7AD1E894EA308C998C0A26489030DFAB0@zeus.epicgames.net> I'm looking for insight into general unification problems of the following form: A unification problem consists of an equation within a quantifier prefix. The goal is to characterize the solutions to the unification problem: whether there are none, one, or many possible values for the existential variables which satisfy the equation. (This arises as the core of a typechecking algorithm.) A quantifier prefix is an ordered list of existential and universal quantifiers without explicit bounds. Example: Ex.Ay.Ez. means "There exists an x such that, for all y, there exists a z such that ". An equation is one of: - An equality between two terms (t1 = t2) - A conjunction of two equations (e1 and e2) - A disjunction of two equations (e1 or e2) - A negation of an equation (not e1) A term is one of: - A variable (x, y, z, ...) bound by the quantifier prefix. - A lambda expression taking one term to another term (t1->t2). We can also add constants (0, 1, 2...) to terms, without changing the expressive power (else we can encode them as Church numerals). Example unification problems: - Ex.x=1 - one solution - Ex.x=1 and x=2 - no solution - Ay.Ex.x=y - infinitely many solutions - Ex.Ay.x=y - no solutions - Ex.Ey.not x=y - infinitely many solutions - Ef.Ay.f=(y->y) -- one solution (f is the identity function) - Ef.f=(2->3) -- infinitely many solutions (f comprises all functions taking 2 to 3) - Ef.f=(0->1) & (2->7) -- infinitely many solutions (all functions taking 0 to 1, and 2 to 7) - Ef.Ay.f=(y->y) and f=(2->3) -- no solutions (the identity function doesn't take 2 to 3) - Ex.Ay.x=1 or x=y - one solution - Ef.Ax.not f=(0->x) -- f is all functions that don't have 0 in their domain Since the resulting system is Turing-complete, we can't expect to find a decision procedure. But a partial decision procedure would be very useful, and it seems (intuitively) like we could define a well-founded subset of the problem and give a decision procedure over it. Better yet would be a decision algorithm which happens to always terminate for well-founded problems, and diverge for (some) others. Any references, or suggestions on how to proceed? Thanks! Tim Sweeney Epic Games From alwen.tiu at rsise.anu.edu.au Mon May 21 20:55:22 2007 From: alwen.tiu at rsise.anu.edu.au (Alwen Tiu) Date: Tue, 22 May 2007 10:55:22 +1000 Subject: [TYPES] Unification within a quantifier prefix In-Reply-To: <8A4FE0C7AD1E894EA308C998C0A26489030DFAB0@zeus.epicgames.net> References: <8A4FE0C7AD1E894EA308C998C0A26489030DFAB0@zeus.epicgames.net> Message-ID: <46523F7A.2040504@rsise.anu.edu.au> You might want to check the following paper. It addresses the type of unification problem you mentioned. Dale Miller. Unification Under a Mixed Prefix. Journal of Symbolic Computation 14(4), 1992. -Alwen Tim Sweeney wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I'm looking for insight into general unification problems of the > following form: > > A unification problem consists of an equation within a quantifier > prefix. The goal is to characterize the solutions to the unification > problem: whether there are none, one, or many possible values for the > existential variables which satisfy the equation. (This arises as the > core of a typechecking algorithm.) > > A quantifier prefix is an ordered list of existential and universal > quantifiers without explicit bounds. Example: Ex.Ay.Ez. means > "There exists an x such that, for all y, there exists a z such that > ". > > An equation is one of: > - An equality between two terms (t1 = t2) > - A conjunction of two equations (e1 and e2) > - A disjunction of two equations (e1 or e2) > - A negation of an equation (not e1) > > A term is one of: > - A variable (x, y, z, ...) bound by the quantifier prefix. > - A lambda expression taking one term to another term (t1->t2). > > We can also add constants (0, 1, 2...) to terms, without changing the > expressive power (else we can encode them as Church numerals). > > Example unification problems: > > - Ex.x=1 - one solution > - Ex.x=1 and x=2 - no solution > - Ay.Ex.x=y - infinitely many solutions > - Ex.Ay.x=y - no solutions > - Ex.Ey.not x=y - infinitely many solutions > - Ef.Ay.f=(y->y) -- one solution (f is the identity function) > - Ef.f=(2->3) -- infinitely many solutions (f comprises all functions > taking 2 to 3) > - Ef.f=(0->1) & (2->7) -- infinitely many solutions (all functions > taking 0 to 1, and 2 to 7) > - Ef.Ay.f=(y->y) and f=(2->3) -- no solutions (the identity function > doesn't take 2 to 3) > - Ex.Ay.x=1 or x=y - one solution > - Ef.Ax.not f=(0->x) -- f is all functions that don't have 0 in their > domain > > Since the resulting system is Turing-complete, we can't expect to find a > decision procedure. But a partial decision procedure would be very > useful, and it seems (intuitively) like we could define a well-founded > subset of the problem and give a decision procedure over it. Better yet > would be a decision algorithm which happens to always terminate for > well-founded problems, and diverge for (some) others. > > Any references, or suggestions on how to proceed? > > Thanks! > > Tim Sweeney > Epic Games > From Belaid.Benhamou at cmi.univ-mrs.fr Fri May 25 11:11:02 2007 From: Belaid.Benhamou at cmi.univ-mrs.fr (benhamou) Date: Fri, 25 May 2007 17:11:02 +0200 Subject: [TYPES] Call for participation: TABLEAUX 2007 In-Reply-To: <4636257B.5040500@cmi.univ-mrs.fr> References: <200601291711.k0THB45e018819@birkhoff.cas.mcmaster.ca> <458C0FEC.4030407@cmi.univ-mrs.fr> <45BA3081.6040905@cmi.univ-mrs.fr> <4636257B.5040500@cmi.univ-mrs.fr> Message-ID: <4656FC86.7080109@cmi.univ-mrs.fr> We apologize for multiple copies of this CFP ------------------------------------------------------------ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Call for Participation %% %% %% %% TABLEAUX 2007 %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% International Conference TABLEAUX 2007 Automated Reasoning with Analytic Tableaux and Related Methods Aix en Provence, France 3-6 July 2007 http://tableaux2007.univ-cezanne.fr/ GENERAL INFORMATION This conference is the 16th in a series of international meetings on Automated Reasoning with Analytic Tableaux and Related Methods. TOPICS Tableau methods are a convenient formalism for automating deduction in various non-standard logics as well as in classical logic. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, and system diagnosis. The conference brings together researchers interested in all aspects - theoretical foundations, implementation techniques, systems development and applications - of the mechanization of reasoning with tableaux and related methods. INVITED SPEAKERS: Piero Bonatti, Universit? di Napoli John-Jules Meyer, Utrecht University Cesare Tinelli, University of Iowa TUTORIALS: The Tableau Work Bench: Theory and Practice (P. Abate, R. Gor?) Tableau Methods for Interval Temporal Logics (V. Goranko, A. Montanari) Semistructured Databases and Modal Logic (S. Cerrito) COLOCATED WORKSHOP: AGENTS, LOGIC AND THEOREM PROVING 3 July 2007, http://www.lif-sud.univ-mrs.fr/~schwind/Agentws.html ON-LINE REGISTRATION is now open at: http://tableaux2007.univ-cezanne.fr Due to the very high turistic actvity in Aix in July, the availability of hotel rooms is not guaranteed. We strongly suggest anybody who is interested in participating in the Conference to make his/her own hotel reservation as soon as possible, following the directions for accommodations found in the web site of the conference. Bela?d Benhamou Publicity Chair From naumann at cs.stevens.edu Wed Jun 6 12:18:11 2007 From: naumann at cs.stevens.edu (David Naumann) Date: Wed, 6 Jun 2007 12:18:11 -0400 (EDT) Subject: [TYPES] Formal proof of type-soundness for references in Coq In-Reply-To: <54f15b6e0702091916m1d18f8e5n83d2d45c36deabb6@mail.gmail.com> References: <54f15b6e0702091916m1d18f8e5n83d2d45c36deabb6@mail.gmail.com> Message-ID: On Fri, 9 Feb 2007, mulhern wrote: > Date: Fri, 9 Feb 2007 21:16:37 -0600 > From: mulhern > To: types-list at lists.seas.upenn.edu, coq-club at pauillac.inria.fr > Subject: [TYPES] Formal proof of type-soundness for references in Coq > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hi! > > I've posted a formal proof in Coq of type-soundness for references at > http://www.cs.wisc.edu/~mulhern/proofs/type-soundness/references.html. > > I think it might be interesting to people on the Coq list because it uses > the module system. > > As far as I know, there is no other publicly available formal proof of > type-soundness for references available, so it might be interesting to > people on the types list as well. > > -mulhern There was a follow-up clarifying Mulhern's interest in proof fragments, and one from Crary on the formalization of Standard ML in POPL07. For the record, there's other machine-checked work on languages with references, e.g., Nipkow's group has done type soundness for a fragment of Java using Isabelle/HOL. For a language comparable to Middleweight Java [Parkinson,Pitts], I prove type soundness in PVS [TPHOLS 05]. The semantics is denotational, and type soundness is expressed as well-definedness of the semantic function, which has a dependent type expressing well-formedness of states and absence of dangling references. (It's an ancillary result since my main purpose is a noninterference theorem for security typing.) That PVS model has been extended to include Java's 'interface types' and first-class exceptions and handlers. The domains are streamlined to facilitate logical relations proofs. Type soundness has been proved as before. This development is being used to formalize the JML specification language [Corejml 06]. The PVS source files are available online. http://www.cs.stevens.edu/~naumann/publications/ [TPHOLS 05] author = {David A. Naumann}, title = {Verifying a Secure Information Flow Analyzer}, year = 2005, booktitle = {18th International Conference on Theorem Proving in Higher Order Logics {TPHOLS}}, editor = {Joe Hurd and Tom Melham}, pages = {211--226}, publisher = {Springer}, series = LNCS, volume = 3603 [Corejml 06] title={Preliminary Definition of Core {JML}}, author={Gary T. Leavens and David A. Naumann and Stan Rosenberg}, institition={Stevens Institute of Technology}, number={CS Report 2006-07}, URL={http://www.cs.stevens.edu/~naumann/SIT-TR-2006-07a.pdf} From david.hopwood at industrial-designers.co.uk Wed Jun 6 18:31:50 2007 From: david.hopwood at industrial-designers.co.uk (David Hopwood) Date: Wed, 06 Jun 2007 23:31:50 +0100 Subject: [TYPES] Formal proof of type-soundness for references in Coq In-Reply-To: References: <54f15b6e0702091916m1d18f8e5n83d2d45c36deabb6@mail.gmail.com> Message-ID: <466735D6.4060300@industrial-designers.co.uk> David Naumann wrote: > [Corejml 06] > title={Preliminary Definition of Core {JML}}, > author={Gary T. Leavens and David A. Naumann and Stan Rosenberg}, > institition={Stevens Institute of Technology}, > number={CS Report 2006-07}, > URL={http://www.cs.stevens.edu/~naumann/SIT-TR-2006-07a.pdf} Should be . -- David Hopwood From nvk at cs.ucla.edu Thu Jun 21 00:27:39 2007 From: nvk at cs.ucla.edu (N V Krishna.) Date: Thu, 21 Jun 2007 09:57:39 +0530 Subject: [TYPES] Compiler frameworks. In-Reply-To: References: Message-ID: <634b74b30706202127g1a478704j586975fb9606fbf4@mail.gmail.com> Hello All, I am trying to make a compendium of different compiler frameworks that are available. The frameworks can cater to any aspect of compiling (Parsing / analysis / verification/ optimization/ code generation). The problem is that of plenty. Each framework caters to different needs, but there does not seem to be a single listing of all, possibly with details on what the framework provides and still better with comparisions with other similar ones. Many a times this leads to new researchers either (a) using some not-so-suitable-for-his-or-her-purpose framework or (b) coming up with new frameworks. I propose to making a public webpage, where all such frameworks can be listed (If, some such page already exists, then please inform me). I would be greatful, if each one of you, could take a few minutes and write about (a) the compiler frameworks that you might have developed/used and optionally (b) any comments you have about the framework(s) (+/-). On my part, I promise to compile this webpage and make it public. Warm regards, N V Krishna. From eeide at cs.utah.edu Thu Jun 21 10:03:12 2007 From: eeide at cs.utah.edu (Eric Eide) Date: Thu, 21 Jun 2007 08:03:12 -0600 Subject: [TYPES] Compiler frameworks. In-Reply-To: N V Krishna.'s message of Thursday, June 21 2007 <634b74b30706202127g1a478704j586975fb9606fbf4@mail.gmail.com> References: <634b74b30706202127g1a478704j586975fb9606fbf4@mail.gmail.com> Message-ID: <18042.34080.642842.567536@bas.flux.utah.edu> N V Krishna writes: > I am trying to make a compendium of different compiler frameworks > that are available. The frameworks can cater to any aspect of > compiling (Parsing / analysis / verification/ optimization/ code > generation). The problem is that of plenty. Each framework caters > to different needs, but there does not seem to be a single listing of > all, [...] You might want to look at the "catalog of free compilers" and the "directory of commercial compiler tools" that are associated with the `comp.compilers' USENET newsgroup. The catalogs are a bit dated, but perhaps better than starting from scratch. Good luck --- Eric. -- ------------------------------------------------------------------------------- Eric Eide . University of Utah School of Computing http://www.cs.utah.edu/~eeide/ . +1 (801) 585-5512 voice, +1 (801) 581-5843 FAX From angray at beeb.net Sat Jun 23 11:08:06 2007 From: angray at beeb.net (Aaron Gray) Date: Sat, 23 Jun 2007 16:08:06 +0100 Subject: [TYPES] Compiler frameworks. References: <634b74b30706202127g1a478704j586975fb9606fbf4@mail.gmail.com> Message-ID: <004001c7b5a8$4e9aced0$0300a8c0@amd2500> >[ The Types Forum, >http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hello All, > I am trying to make a compendium of different compiler frameworks that > are available. The frameworks can cater to any aspect of compiling > (Parsing / analysis / verification/ optimization/ code generation). > The problem is that of plenty. Each framework caters to different > needs, but there does not seem to be a single listing of all, possibly > with details on what the framework provides and still better with > comparisions with other similar ones. Many a times this leads to new > researchers either (a) using some > not-so-suitable-for-his-or-her-purpose framework or (b) coming up with > new frameworks. > > I propose to making a public webpage, where all such frameworks can be > listed (If, some such page already exists, then please inform me). I > would be greatful, if each one of you, could take a few minutes and > write about (a) the compiler frameworks that you might have > developed/used and optionally (b) any comments you have about the > framework(s) (+/-). > > On my part, I promise to compile this webpage and make it public. You can add 'Prop' :- http://prop-cc.sourceforge.net/leunga/www/prop.html Compilers.net is one of the best lists :- http://www.compilers.net/ Regards, Aaron From leaf.petersen at intel.com Tue Jul 3 21:33:49 2007 From: leaf.petersen at intel.com (Petersen, Leaf) Date: Tue, 3 Jul 2007 18:33:49 -0700 Subject: [TYPES] CFP: DAMP 2008 Message-ID: <470B3ABB95B22D42B272B227A8B0CF47CB63B6@scsmsx415.amr.corp.intel.com> DAMP 2008: Workshop on Declarative Aspects of Multicore Programming San Francisco, CA, USA (colocated with POPL 2008) Parallelism is going mainstream. Many chip manufactures are turning to multicore processor designs rather than scalar-oriented frequency increases as a way to get performance in their desktop, enterprise, and mobile processors. This endeavor is not likely to succeed long term if mainstream applications cannot be parallelized to take advantage of tens and eventually hundreds of hardware threads. Multicore architectures will differ in significant ways from their multisocket predecessors. For example, the communication to compute bandwidth ratio is likely to be higher, which will positively impact performance. More generally, multicore architectures introduce several new dimensions of variability in both performance guarantees and architectural contracts, such as the memory model, that may not stabilize for several generations of product. Programs written in functional or logic programming languages, or even in other languages with a controlled use of side effects, can greatly simplify parallel programming. Such declarative programming allows for a deterministic semantics even when the underlying implementation might be highly non-deterministic. In addition to simplifying programming this can simplify debugging and analyzing correctness. DAMP is a one-day workshop seeking to explore ideas in programming language design that will greatly simplify programming for multicore architectures, and more generally for tightly coupled parallel architectures. The emphasis will be on functional and logic programming, but any programming language ideas that aim to raise the level of abstraction are welcome. DAMP seeks to gather together researchers in declarative approaches to parallel programming and to foster cross fertilization across different approaches. Specific topics include, but are not limited to: * suitability of functional and logic programming languages to multicore applications; * run-time issues such as garbage collection or thread scheduling; * architectural features that may enhance the parallel performance of declarative languages; * type systems and analysis for accurately knowing or limiting dependencies, aliasing, effects, and nonpure features; * ways of specifying or hinting at parallelism; * ways of specifying or hinting at data placement which abstract away from any details of the machine; * compiler techniques, automatic parallelization, automatic granularity control; * experiences of and challenges arising from making declarative programming practical; * technology for debugging parallel programs; * design and implementation of domain-specific declarative languages for multi-core; Submission details are TBA. Expected submission deadline: early October. Programm Chair: Manuel Hermenegildo Technical University of Madrid / IMDEA-Software -- herme at fi.upm.es University of New Mexico -- herme at unm.edu Programme Committee: TBA General Chairs: Leaf Petersen Neal Glew Intel Corporation Santa Clara, CA, USA leaf.petersen at intel.com neal.glew at intel.com Planned URL (in construction): http://www.cliplab.org/Conferences/DAMP08 Past DAMPs: http://glew.org/damp2006 http://www.cs.cmu.edu/~damp From ohori at riec.tohoku.ac.jp Wed Jul 4 04:09:16 2007 From: ohori at riec.tohoku.ac.jp (Atsushi Ohori) Date: Wed, 04 Jul 2007 17:09:16 +0900 (JST) Subject: [TYPES] a paper available on "Record Unboxing", a new type-based optimization Message-ID: <20070704.170916.719889242.ohori@riec.tohoku.ac.jp> Dear Colleagues, Some of the types-list readers may be interested in the following paper, which shows a new type-based optimization method that "unboxes" tuples/records by flattening component tuples and changing top-level tuples to multiple value passing. The required type based analysis is simple but the resulting method shown to be quite effective. This is implemented in the SML# (an extension of the Standard ML) compiler version 0.30, which is available from: http://www.pllab.riec.tohoku.ac.jp/smlsharp/ Any comments are welcome. Best regards, Atsushi -------------------------------------------------------------------- Record Unboxing Huu-Duc Nguyen and Atsushi Ohori RIEC, Tohoku University http://www.pllab.riec.tohoku.ac.jp/~ohori/research/RecordUnboxing.pdf In the conventional implementation of functional languages, tuples (records) are uniformly implemented as heap allocated objects even when they are used only for multiple parameter passing. This paper develops a type-based ``record unboxing'' optimization method that reduces the overhead due to those unnecessary heap allocation and associated memory accesses. We first develops a type-based algorithm that infers where each record expression is ``rigid'' or not, i.e. it requires heap allocation or not based on the observation that change of a representation of a record type that does not interact with the external environment does not affect the behavior of the program. We then develop a record unboxing algorithm that transforms a functional language with records to a multiple value calculus in which a function can take/return multiple values by transforming all non rigid records into multiple values. The combination of the two yields a simple and yet surprisingly effective optimization method. We have implemented the proposed method in a compiler for full Standard ML language, and have evaluated it with a typical benchmark programs. The results show significant speed ups for non trivial benchmarks, including 21% speed up of mlyacc and 27% speed up for lexgen. From paramr at gmail.com Tue Jul 10 14:26:46 2007 From: paramr at gmail.com (Param Jyothi Reddy) Date: Tue, 10 Jul 2007 11:26:46 -0700 Subject: [TYPES] Proof term for proof by exhaustion Message-ID: Hi, Lets define vector in usual way with constructors: nil : Vector T 0 cons : Vector T n -> T -> Vector T (S n) along with its inductive elimination rule. Let BD be type of Binary Digits (enumeration with elements 0 and 1). Also lets say i have proofs of some predicate P for all elements of Vector's over BD of length 2, i.e. p_0 : P(00), p_1 : P(01), p_2 : P(10), p_3 : P(11), where bd is cons (cons nil d) b. using these How will the proof term for (forall v : Vector BD (S S 0) ). P(v) look like? I can use or elimination if i could build proof for: (forall v : Vector BD (S S 0)). v == 00 or v == 01 or v == 10 or v == 11. However i am not sure how the proof term for this looks either. Can someone help me understand this? Thanks, Param From paramr at gmail.com Tue Jul 10 18:55:14 2007 From: paramr at gmail.com (Param Jyothi Reddy) Date: Tue, 10 Jul 2007 15:55:14 -0700 Subject: [TYPES] [Coq-Club] Proof term for proof by exhaustion In-Reply-To: <1331FE89-B728-447D-B899-C4776C357C9C@inria.fr> References: <1331FE89-B728-447D-B899-C4776C357C9C@inria.fr> Message-ID: Hi Benjamin, I wanted to look at how the actual proof term (in terms of raw CIC/PTS type system) looks like rather than using tactics. More from perspective of understanding type system. The essential point is how can we express the fact that vector of length 2 are just 00,01,10 and 11 (nothing more/nothing less)? Param On 7/10/07, Benjamin Werner wrote: > You need to generalize your statement, so that it makes sense for > vectors of any length. > > For instance: > > Parameter P : (Vector bool 2) -> Prop. > > Definition PP (n : nat) : Vector bool n -> Prop := > match n as n return Vector bool n -> Prop with > | (S (S O)) => fun p => (P p) > | _ => fun _ => True > end. > > Goal forall n p, PP n p. > intros n p; case p; simpl; trivial; > clear n p; intros n v [|]; case v; trivial; > clear n v; intros n v [|]; case v; trivial. > ... > > > Cheers, > > B > > > Le 10 juil. 07 ? 20:26, Param Jyothi Reddy a ?crit : > > > Hi, > > Lets define vector in usual way with constructors: > > nil : Vector T 0 > > cons : Vector T n -> T -> Vector T (S n) > > > > along with its inductive elimination rule. Let BD be type of Binary > > Digits (enumeration with elements 0 and 1). > > > > Also lets say i have proofs of some predicate P for all elements of > > Vector's over BD of length 2, i.e. > > > > p_0 : P(00), p_1 : P(01), p_2 : P(10), p_3 : P(11), where bd is cons > > (cons nil d) b. > > > > using these How will the proof term for > > > > (forall v : Vector BD (S S 0) ). P(v) look like? > > > > > > I can use or elimination if i could build proof for: > > > > (forall v : Vector BD (S S 0)). v == 00 or v == 01 or v == 10 or v == > > 11. However i am not sure how the proof term for this looks either. > > > > Can someone help me understand this? > > > > Thanks, > > Param > > > > -------------------------------------------------------- > > Bug reports: http://coq.inria.fr/bin/coq-bugs > > Archives: http://pauillac.inria.fr/pipermail/coq-club > > http://pauillac.inria.fr/bin/wilma/coq-club > > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club > > From Malcolm.Tyrrell at computing.dcu.ie Tue Jul 17 10:25:55 2007 From: Malcolm.Tyrrell at computing.dcu.ie (Malcolm Tyrrell) Date: Tue, 17 Jul 2007 15:25:55 +0100 Subject: [TYPES] Completeness of powersimulation Message-ID: <469CD173.70008@computing.dcu.ie> Hi there. I'm not sure that this is the appropriate forum for my question, so I apologise if it seems off-topic. If you can think of a more suitable forum, please tell me. Powersimulation is a sound technique for establishing data refinement in theories of predicate transformers. There is a completeness result for powersimulation (originally in [1] and reworked in [2]), but it is subject to a few awkward conditions. In particular, abstract data types may not use unbounded nondeterminacy. Can anyone tell me if it is known whether the conditions are necessary? If not, can anyone provide an example of the incompleteness of powersimulation? The language of [2] (p223) gives the impression that the conditions are necessary. However, this is not clearly stated. References: [1] "A Single Complete Rule for Data Refinement", Paul H. B. Gardiner and Carroll Morgan, Formal Asp. Comput. 1993 [2] "Data Refinement: Model-Oriented Proof Methods and Their Comparison", W. de Roever and Kai Engelhardt, Cambridge University Press, 1999 Thanks for any help, Malcolm. From paramr at gmail.com Mon Jul 30 01:30:03 2007 From: paramr at gmail.com (Param Jyothi Reddy) Date: Sun, 29 Jul 2007 22:30:03 -0700 Subject: [TYPES] Inconsistency and non dependent sum elimination Message-ID: Hi, This is in the context for impredicative Prop and predicative type hierarchy. The base type system is PTS. I was reading that in presence of dependent elimination for sum type, elimination from Prop sort to Type sort can lead to inconsistency in logic. Would it also hold true if we allow only non-dependent elimination i.e. eliminating Prop into Type without depedency. SumDependentCase Rule: (inconsistent) C[z] : Type c1[x] : C[Inj_1(x)] c2[y] : C[Inj_2(y)] k : A+B A + B : Prop ---------------------------------------------------------------------------------------------------------------- [G, x:A, y:B, z:A+B] +~(k, [x:A]c1[x], [y:B]c2[y], [z:A+B]C[z]) : C[k] SumDependentCase Rule: (consistent??) C : Type c1 : C c2 : C k : A+B A + B : Prop ----------------------------------------------------------------------------- [G, x:A, y:B, z:A+B] +~(k, [x:A]c1, [y:B]c2, z:A+B) : C Would same be true for dependent Sum (Sigma) type? (instead of using direct second projection, using a case similar to the one given for Sum case). Thanks in advance, Param From bsistany at yahoo.ca Thu Aug 16 16:52:05 2007 From: bsistany at yahoo.ca (Bahman Sistany) Date: Thu, 16 Aug 2007 13:52:05 -0700 (PDT) Subject: [TYPES] implementations of fj (Featherweight Java) Message-ID: <204040.38589.qm@web56608.mail.re3.yahoo.com> Dear Colleagues, I am wondering if complete/usable implementations of fj (Featherweight Java) and perhaps fgj (Featherweight Generic Java) exist that are easy to extend/experiment with, preferably in Java and/or Haskell. I have already found a few implementations but rather than go through each of these I thought I'd ask around on this list first. Regards, Bahman Be smarter than spam. See how smart SpamGuard is at giving junk email the boot with the All-new Yahoo! Mail at http://mrd.mail.yahoo.com/try_beta?.intl=ca From matthias at ccs.neu.edu Thu Aug 16 21:52:46 2007 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Thu, 16 Aug 2007 21:52:46 -0400 Subject: [TYPES] implementations of fj (Featherweight Java) In-Reply-To: <204040.38589.qm@web56608.mail.re3.yahoo.com> References: <204040.38589.qm@web56608.mail.re3.yahoo.com> Message-ID: A Redex model of ClassicJava is available from PLT Scheme's PLaneT web repository. Its a direct specification of reduction rules plus a type checker in the usual recursive style. Cut it back and you have FJ. -- Matthias On Aug 16, 2007, at 4:52 PM, Bahman Sistany wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ > types-list ] > > Dear Colleagues, > > I am wondering if complete/usable implementations of fj > (Featherweight Java) and perhaps fgj (Featherweight Generic Java) > exist that are easy to extend/experiment with, preferably in Java > and/or Haskell. I have already found a few implementations but > rather than go through each of these I thought I'd ask around on > this list first. > > Regards, > Bahman > > > > > > Be smarter than spam. See how smart SpamGuard is at giving > junk email the boot with the All-new Yahoo! Mail at http:// > mrd.mail.yahoo.com/try_beta?.intl=ca > From bsistany at yahoo.ca Mon Aug 20 09:20:46 2007 From: bsistany at yahoo.ca (Bahman Sistany) Date: Mon, 20 Aug 2007 06:20:46 -0700 (PDT) Subject: [TYPES] implementations of fj (Featherweight Java) Message-ID: <515929.6039.qm@web56605.mail.re3.yahoo.com> Thanks Andreas and everyone for your help. I may still do my own in which case I will report it back to this list for sure. --Bahman ----- Original Message ---- From: Andreas Abel To: Bahman Sistany Cc: types-list at lists.seas.upenn.edu Sent: Friday, August 17, 2007 5:29:20 AM Subject: Re: [TYPES] implementations of fj (Featherweight Java) Dear Bahman, here is a Haskell implementation of fj. Compilation requires ghc. Cheers, Andreas Bahman Sistany wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear Colleagues, > > I am wondering if complete/usable implementations of fj (Featherweight Java) and perhaps fgj (Featherweight Generic Java) exist that are easy to extend/experiment with, preferably in Java and/or Haskell. I have already found a few implementations but rather than go through each of these I thought I'd ask around on this list first. > > Regards, > Bahman > > > > > > Be smarter than spam. See how smart SpamGuard is at giving junk email the boot with the All-new Yahoo! Mail at http://mrd.mail.yahoo.com/try_beta?.intl=ca > > -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich http://www.tcs.informatik.uni-muenchen.de/~abel/ Be smarter than spam. See how smart SpamGuard is at giving junk email the boot with the All-new Yahoo! Mail at http://mrd.mail.yahoo.com/try_beta?.intl=ca From wadler at inf.ed.ac.uk Tue Aug 21 04:32:41 2007 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Tue, 21 Aug 2007 09:32:41 +0100 Subject: [TYPES] Encoding of negation Message-ID: <4A9BD430-50F0-4E01-A55D-B110A49DFCC8@inf.ed.ac.uk> One possible encoding of negation, closely related to the CPS translation, is the following: A* = all Z. A+ X+ = X (A -> B)+ = A+ -> B+ (not A)+ = A+ -> Z where Z is a fresh type variable that does not appear free in A. I conjecture that A1, ..., An |- B holds in classical logic iff A1*, ..., An* |- B* holds in intuitionistic logic. Has anyone explored this translation? As an example of its interest, I conjecture that A* and (not (not A))* are isomorphic in the presence of parametricity; this is certainly true if A contains no negations. Many thanks for any responses. Cheers, -- P From carter.schonwald at yale.edu Tue Aug 21 12:36:46 2007 From: carter.schonwald at yale.edu (Carter Tazio Schonwald) Date: Tue, 21 Aug 2007 12:36:46 -0400 Subject: [TYPES] Encoding of negation In-Reply-To: <4A9BD430-50F0-4E01-A55D-B110A49DFCC8@inf.ed.ac.uk> References: <4A9BD430-50F0-4E01-A55D-B110A49DFCC8@inf.ed.ac.uk> Message-ID: <46CB149E.50202@yale.edu> I believe that this paper http://www.cs.bham.ac.uk/~hxt/research/effects.pdf by Hayo Thielecke studies this style of translation and its use in the presence of effects cheers, -Carter Philip Wadler wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > One possible encoding of negation, closely related to the CPS > translation, is the following: > > A* = all Z. A+ > > X+ = X > (A -> B)+ = A+ -> B+ > (not A)+ = A+ -> Z > > where Z is a fresh type variable that does not appear free in A. I > conjecture that > > A1, ..., An |- B > > holds in classical logic iff > > A1*, ..., An* |- B* > > holds in intuitionistic logic. > > Has anyone explored this translation? As an example of its interest, > I conjecture that A* and (not (not A))* are isomorphic in the > presence of parametricity; this is certainly true if A contains no > negations. > > Many thanks for any responses. Cheers, -- P > > > > > From Burak.Emir at epfl.ch Tue Aug 21 12:41:15 2007 From: Burak.Emir at epfl.ch (Burak Emir) Date: Tue, 21 Aug 2007 18:41:15 +0200 Subject: [TYPES] Encoding of negation In-Reply-To: <4A9BD430-50F0-4E01-A55D-B110A49DFCC8@inf.ed.ac.uk> References: <4A9BD430-50F0-4E01-A55D-B110A49DFCC8@inf.ed.ac.uk> Message-ID: Krivine has written about this translation [1] and the mentioned result appears as theorem 3.2 (without proof). He calls it Goedel's translation and the paper is about storage operators that are specific to a data type and serve the purpose of simulating call-by-value in call-by-name. [1] Jean-Louis Krivine, Operateurs de mise en memoire et traduction de Goedel, Arch. Math. Logic (1990) 30:241--267, Springer http://www.springerlink.com/content/t420j01286833044/ Could this be what you were looking for? cheers, Burak On 8/21/07, Philip Wadler wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list] > > One possible encoding of negation, closely related to the CPS > translation, is the following: > > A* = all Z. A+ > > X+ = X > (A -> B)+ = A+ -> B+ > (not A)+ = A+ -> Z > > where Z is a fresh type variable that does not appear free in A. I > conjecture that > > A1, ..., An |- B > > holds in classical logic iff > > A1*, ..., An* |- B* > > holds in intuitionistic logic. > > Has anyone explored this translation? As an example of its interest, > I conjecture that A* and (not (not A))* are isomorphic in the > presence of parametricity; this is certainly true if A contains no > negations. > > Many thanks for any responses. Cheers, -- P > > > -- Burak Emir Research Assistant / PhD Candidate Programming Methods Group EPFL, 1015 Lausanne, Switzerland http://lamp.epfl.ch/~emir From v.komendantsky at bcri.ucc.ie Thu Aug 23 08:09:07 2007 From: v.komendantsky at bcri.ucc.ie (Vladimir Komendantsky) Date: Thu, 23 Aug 2007 14:09:07 +0200 Subject: [TYPES] Re: Encoding of negation In-Reply-To: <20070822214133.GA3244@eire.artimon> References: <20070822214133.GA3244@eire.artimon> Message-ID: <46CD78E3.9020304@bcri.ucc.ie> >One possible encoding of negation, closely related to the CPS >translation, is the following: > > A* = all Z. A+ > > X+ = X > (A -> B)+ = A+ -> B+ > (not A)+ = A+ -> Z > >where Z is a fresh type variable that does not appear free in A. > A closely related call-by-name CPS translation was described, e.g., in Peter Selinger's "Control categories and duality: on the categorical semantics of the lambda-mu calculus" (2001), http://www.mscs.dal.ca/~selinger/papers/control.pdf There, in Section 6.1, he gives the CPS translation which, if we content ourselves with the case above, gives the following rules for translation of types: A* = A+ -> R X+ = X (A->B)+ = A+ -> B+ (not A)+ = A+ -> R where R is a free fixed type variable (the type of responses). The difference is in A* which now has an occurrence of R in it. So, for example, the law of double negation elimination (not (not A)) |- A is translated as ((A+ -> R) -> R) -> R |- A+ -> R. Since this translation is call-by-name, it is not directly related to Hayo Thieleke's CPS translation, which is call-by-value. The idea behind the call-by-name CPS translation stems back to Goedel's double negation translation. The variants of the CPS call-by-value translation correspond (sometimes loosely) to Kolmogorov's double negation translation. As noted by Hayo Thieleke, in the absence of control types (which is exactly the case) one has universal quantification, "all Z", instread of just the free variable R. >I conjecture that > > A1, ..., An |- B > >holds in classical logic iff > > A1*, ..., An* |- B* > >holds in intuitionistic logic. > > > For Peter Selinger's translation above this holds if we rewrite R with _|_. But if we let A* = all Z. A+ (and don't rewrite response variables) we obtain the following translation of the double negation elimination: all Z. (A+ -> Z) -> Z) |- all Z. A+ This is not provable already in classical logic (otherwise (A\/B)->A would be provable). In this sence the above conjecture does not hold. -- Vladimir From wadler at inf.ed.ac.uk Fri Aug 24 14:34:13 2007 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Fri, 24 Aug 2007 19:34:13 +0100 Subject: [TYPES] Encoding of negation In-Reply-To: <20070821155958.GA29523@cs.cmu.edu> References: <4A9BD430-50F0-4E01-A55D-B110A49DFCC8@inf.ed.ac.uk> <20070821155958.GA29523@cs.cmu.edu> Message-ID: Many thanks to Alex Simpson, Noam Zeilberger, and Hasegawa Masahito for pointing out that my conjecture cannot be correct (see below), and to Carter Schonwald, Burak Emir, Thomas Streicher, and Vladimir Komendanstsky for pointing to results related to the conjecture. Any other pointers appreciated. Cheers, -- P On 21 Aug 2007, at 16:59, Noam Zeilberger wrote: >> One possible encoding of negation, closely related to the CPS >> translation, is the following: >> >> A* = all Z. A+ >> >> X+ = X >> (A -> B)+ = A+ -> B+ >> (not A)+ = A+ -> Z >> >> where Z is a fresh type variable that does not appear free in A. I >> conjecture that >> >> A1, ..., An |- B >> >> holds in classical logic iff >> >> A1*, ..., An* |- B* >> >> holds in intuitionistic logic. > > I don't think the above is the right translation of implication, > because this conjecture is easily falsified by negation-free > classical theorems which are not intuitionistic. For example, > Pierce's law P = ((X -> Y) -> X) -> X is valid classically, > but P* = all Z.P is not valid intuitionistically. > > I guess a natural fix would be to use > > (A -> B)+ = A+ -> (B+ -> Z) -> Z > > Then the translation of Pierce's law becomes: > > P* = all Z.((X -> (Y -> Z) -> Z) -> (X -> Z) -> Z) -> (X -> Z) -> Z > > Kind of an eyesore, but indeed intuitionistically valid. > > Noam From rowan at csse.uwa.edu.au Fri Aug 24 14:40:07 2007 From: rowan at csse.uwa.edu.au (Rowan Davies) Date: Sat, 25 Aug 2007 02:40:07 +0800 Subject: [TYPES] Encoding of negation In-Reply-To: <46CD78E3.9020304@bcri.ucc.ie> References: <20070822214133.GA3244@eire.artimon> <46CD78E3.9020304@bcri.ucc.ie> Message-ID: I agree with Vladimir, although I would also offer the following slightly more direct counterexample for the conjecture: If we consider A = (not A1) -> A2 with A1 and A2 not containing 'not' then A* = all Z. (A1 -> Z) -> A2 (since A1*=A1and A2*= A2, in the absence of not) In this case, the conjecture (with an empty context) would assert the equivalence between the first (in IL) and the second (in CL). But, the second is logically equivalent to A2, since choosing p=A1 yields (A1 -> A1) which forces A2, and p does not appear in A2, hence it must be true independent of p. So, the conjecture would relate: (not A1) -> A2 with A2 This seems very unlikely between any two reasonable logics, given that the second is independent of A1. Having said that, I see the motivation in making the conjecture, and considering that it holds for an important case, I wonder: How large is the set of formulas/type for which it holds? From wadler at inf.ed.ac.uk Sat Aug 25 05:59:54 2007 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Sat, 25 Aug 2007 10:59:54 +0100 Subject: [TYPES] [Fwd: Re: Encoding of negation] In-Reply-To: <46CD7302.3060804@sophia.inria.fr> References: <46CD7302.3060804@sophia.inria.fr> Message-ID: <41E6CB13-8A5D-45C8-A117-B2B41D8C935A@inf.ed.ac.uk> > A closely related call-by-name CPS translation was described, e.g., > in Peter Selinger's > "Control categories and duality: on the categorical semantics of > the lambda-mu calculus" (2001), > http://www.mscs.dal.ca/~selinger/papers/control.pdf > > There, in Section 6.1, he gives the CPS translation which, if we > content ourselves with the case above, gives the following rules > for translation of types: > > A* = A+ -> R > X+ = X > (A->B)+ = A+ -> B+ > (not A)+ = A+ -> R > > where R is a free fixed type variable (the type of responses). The > difference is in A* which now has an occurrence of R in it. So you are suggesting that my conjecture may hold if we modify it as follows: A* = all Z. A+ -> Z A+ as before This in effect adds a negation, so I would no longer expect that A1,...,An |- B classically iff A1*,...,An* |- B* intuitionistically, although I might expect that A |- B classically iff B* |- A* intuitionistically. Is that what you had in mind? > But if we let > > A* = all Z. A+ > > (and don't rewrite response variables) we obtain the following > translation of the double negation elimination: > > all Z. (A+ -> Z) -> Z) |- all Z. A+ > > This is not provable already in classical logic (otherwise (A\/B)- > >A would be provable). In this sence the above conjecture does not > hold. Why do you claim that if the above is provable then (A\/B)->A is provable? Note that in the case where A does not contain negation, all Z. (A+ -> Z) -> Z is isomorphic to A, in the presence of parametricity. Cheers, -- P From v.komendantsky at bcri.ucc.ie Sat Aug 25 12:37:34 2007 From: v.komendantsky at bcri.ucc.ie (Vladimir Komendantsky) Date: Sat, 25 Aug 2007 18:37:34 +0200 Subject: [TYPES] Encoding of negation In-Reply-To: <41E6CB13-8A5D-45C8-A117-B2B41D8C935A@inf.ed.ac.uk> References: <46CD7302.3060804@sophia.inria.fr> <41E6CB13-8A5D-45C8-A117-B2B41D8C935A@inf.ed.ac.uk> Message-ID: <20070825163734.GA3463@eire.artimon> On Sat, Aug 25, 2007 at 10:59:54AM +0100, Philip Wadler wrote: > So you are suggesting that my conjecture may hold if we modify it as > follows: > > A* = all Z. A+ -> Z > > A+ as before No, even then your conjecture wouldn't hold, as you do note below: > This in effect adds a negation, so I would no longer expect > that A1,...,An |- B classically iff A1*,...,An* |- B* > intuitionistically, > although I might expect that A |- B classically iff B* |- A* > intuitionistically. You couldn't have ever expected Gamma |- B classically iff Gamma* |- B* intuitionistically because this is false for your definition of *. Your point about A |- B iff B* |- A* is fair. This can certainly be exploited for a number of purposes. > Why do you claim that if the above is provable then (A\/B)->A is > provable? Note that in the case where A does not contain negation, > all Z. (A+ -> Z) -> Z is isomorphic to A, in the presence of > parametricity. I do so because of the following intuitionistic reasoning: 1. all Z. (A+ -> Z) -> Z) |- all Z. A+ 2. (A+ -> B) -> B |- A+ (eliminate "all") 3. (C \/ D) |- (C -> D) -> D (intuitionistic fact) 4. (A+ \/ B) |- A+ (apply transitivity of |- to 3 an 2) 3 and 4 are not related to the direct counterexample, which was noted by Rowan earlier in this discussion. However, 4 shows your translation not being faithful. The direct counterexample is simply 1 and 2. The statement at 1 is neither intuitionistically nor classically provable. 2 is a simplier presentation for 1. -- Vladimir From lgreg.meredith at gmail.com Fri Aug 24 21:41:54 2007 From: lgreg.meredith at gmail.com (Meredith Gregory) Date: Fri, 24 Aug 2007 18:41:54 -0700 Subject: [TYPES] Kothe space models of Haghverdi combinators? Message-ID: <5de3f5ca0708241841m1421943ds4742b83c81de4bd@mail.gmail.com> Well-and-untyped alike, i'm just starting to dig more deeply into the differential lambda calculus models and it occurred to me that a goal-driven way to get into the calculations would be to crank out the Kothe-space models [1][2] of the Haghverdi combinators [3][4]. Does anyone on this list know if anybody has already done these calculations so i can compare my results? Best wishes, --greg [1] http://www.pps.jussieu.fr/~ehrhard/pub/kothe.pdf [2] http://www.pps.jussieu.fr/~ehrhard/pub/difflamb.pdf [3] http://xavier.informatics.indiana.edu/~ehaghver/HS-TCS-04.pdf [4] http://xavier.informatics.indiana.edu/~ehaghver/main7.ps -- L.G. Meredith Managing Partner Biosimilarity LLC 505 N 72nd St Seattle, WA 98103 +1 206.650.3740 http://biosimilarity.blogspot.com From wadler at inf.ed.ac.uk Wed Aug 29 10:29:53 2007 From: wadler at inf.ed.ac.uk (Philip Wadler) Date: Wed, 29 Aug 2007 15:29:53 +0100 Subject: [TYPES] Encoding of negation In-Reply-To: <20070825163734.GA3463@eire.artimon> References: <46CD7302.3060804@sophia.inria.fr> <41E6CB13-8A5D-45C8-A117-B2B41D8C935A@inf.ed.ac.uk> <20070825163734.GA3463@eire.artimon> Message-ID: <46D582E1.8020107@inf.ed.ac.uk> Here is your argument again. 1. all Z. (A+ -> Z) -> Z) |- all Z. A+ 2. (A+ -> B) -> B |- A+ (eliminate "all") I repeat, that even if A+ does not contain Z, it is not permissible to conclude 2 from 1. If you want to conclude 2 from 1, you need to tell me how you derive it. The statement 'eliminate all' is not a correct justification! Yours (frustrated), -- P -- \ Philip Wadler, Professor of Theoretical Computer Science /\ School of Informatics, University of Edinburgh / \ http://homepages.inf.ed.ac.uk/wadler/ From selinger at mathstat.dal.ca Thu Aug 30 23:40:31 2007 From: selinger at mathstat.dal.ca (Peter Selinger) Date: Fri, 31 Aug 2007 00:40:31 -0300 (ADT) Subject: [TYPES] Encoding of negation In-Reply-To: <46CD78E3.9020304@bcri.ucc.ie> Message-ID: <20070831034031.67CE35C28B@chase.mathstat.dal.ca> Dear Vladimir, I missed your post when it first appeared, so sorry for the relatively late reply. Although I love to be cited, I should point out that I was mis-cited in this case, in terms of both credit and content. First, let me clarify that the CPS translation you are refering to is not at all due to me; as I stated in the cited paper, this particular translation is due to Hofmann and Streicher (1997) and Streicher and Reus (1996), and is a variant of the original call-by-name CPS translation of Plotkin (1975). [The variant arises because the translation makes use of products in the target language, whereas Plotkin's translation used only "->"] Also, you actually copied the rules incorrectly; see below. Vladimir Komendantsky wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > >One possible encoding of negation, closely related to the CPS > >translation, is the following: > > > > A* = all Z. A+ > > > > X+ = X > > (A -> B)+ = A+ -> B+ > > (not A)+ = A+ -> Z > > > >where Z is a fresh type variable that does not appear free in A. > > > > A closely related call-by-name CPS translation was described, e.g., in > Peter Selinger's "Control categories and duality: on the categorical > semantics of the lambda-mu calculus" (2001), > http://www.mscs.dal.ca/~selinger/papers/control.pdf > > There, in Section 6.1, he gives the CPS translation which, if we content > ourselves with the case above, gives the following rules for translation > of types: > > A* = A+ -> R > X+ = X > (A->B)+ = A+ -> B+ > (not A)+ = A+ -> R > > where R is a free fixed type variable (the type of responses). The > difference is in A* which now has an occurrence of R in it. In case anybody wondered why these rules don't make any sense (and Phil Wadler has already wondered publicly): the reason is that these are actually *not* the rules that appear in Section 6.1 of my paper. For reference, the correct call-by-name rules (in the case above) are: A* = A+ -> R X+ = X (A->B)+ = (A+ -> R) x B+ (not A)+ = A+ -> R Note the different translation of implication. This translation has the following properties, up to intuitionistic type isomorphism: (A -> B)* ~~ A* -> B* (1) (not A)* ~~ not A* (2) Soundness of the translation is therefore not extremely surprising. The only thing this translation does (for this fragment) is to replace each variable by a negated variable; this makes Peirce's law valid and therefore also gives soundness for classical logic. For the sake of completeness, here are the translations of "and" and "or": (A x B)+ = (A+) + (B+) (A + B)+ = (A+) x (B+) Note that the analog of (1) and (2) holds for "and": (A x B)* ~~ A* x B* (3) However, the corresponding property for "or" fails; we only have (not not A + not not B)* ~~ not not (A* + B*) (4) We also have A* + B* |- (A + B)* (4'), but not the opposite implication. This is at the heart of why this translation is sound from classical to intuitionistic logic. It is slightly tighter than Goedel's double negation translation, which uses (up to type isomorphism) (A + B)* = not not (A* + B*). > So, for example, the law of double negation elimination > > (not (not A)) |- A > > is translated as > > ((A+ -> R) -> R) -> R |- A+ -> R. > > Since this translation is call-by-name, it is not directly related to > Hayo Thieleke's CPS translation, which is call-by-value. The idea behind > the call-by-name CPS translation stems back to Goedel's double negation > translation. The variants of the CPS call-by-value translation > correspond (sometimes loosely) to Kolmogorov's double negation > translation. As noted by Hayo Thieleke, in the absence of control types > (which is exactly the case) one has universal quantification, "all Z", > instread of just the free variable R. > > >I conjecture that > > > > A1, ..., An |- B > > > >holds in classical logic iff > > > > A1*, ..., An* |- B* > > > >holds in intuitionistic logic. > > > > > > > For Peter Selinger's translation above this holds if we rewrite R with > _|_. But if we let > > A* = all Z. A+ > > (and don't rewrite response variables) we obtain the following > translation of the double negation elimination: > > all Z. (A+ -> Z) -> Z) |- all Z. A+ > > This is not provable already in classical logic (otherwise (A\/B)->A > would be provable). In this sence the above conjecture does not hold. This last statement is false, as was already pointed out by Phil Wadler. Of course (all Z. (A+ -> Z) -> Z)) implies (A+ -> A+) -> A+), and therefore A+, and therefore (all Z. A+), in the case where Z does not occur in A+. -- Peter From selinger at mathstat.dal.ca Thu Aug 30 23:45:49 2007 From: selinger at mathstat.dal.ca (Peter Selinger) Date: Fri, 31 Aug 2007 00:45:49 -0300 (ADT) Subject: [TYPES] Encoding of negation In-Reply-To: <20070825163734.GA3463@eire.artimon> Message-ID: <20070831034549.16E355C28B@chase.mathstat.dal.ca> Vladimir Komendantsky wrote: > > You couldn't have ever expected Gamma |- B classically iff Gamma* |- B* > intuitionistically because this is false for your definition of *. It certainly holds for the Hofmann-Streicher-Reus translation, and also for Goedel's translation. The right-to-left implication is trivial in those cases because in each case, A = A** holds classically. -- Peter From E.Ritter at cs.bham.ac.uk Thu Sep 6 03:25:06 2007 From: E.Ritter at cs.bham.ac.uk (Eike Ritter) Date: Thu, 06 Sep 2007 08:25:06 +0100 Subject: [TYPES] Encoding of Negation Message-ID: <46DFAB52.5020001@cs.bham.ac.uk> Dear all, it is also very interesting to consider not only provability but also proofs in the question how to encode negation. Hofmann and Streicher not only give a continuation interpretation of classical logic which has the desired property that A |- B classically iff A* |- B* intuitionistically but also extend this translation to the level of proofs by converting any classical proof of A |- B into an intuitionistic proof of A* |- B*. Extending this correspondence to the level of proofs is subtle. Hofmann and Streicher present a translation of classical proofs for formulae consisting of negation, implication and conjunction. We show in [1] that addition of disjunction is problematic, and that only the addition of classical (multi-conclusioned) disjunction works, not a version of intuitionistic sums. [1] D.J. Pym and E. Ritter. On the semantics of classical disjunction. Journal of Pure and Applied Algebra, vol 159, pp. 315--338. David Pym and Eike Ritter From Lengrand at LIX.Polytechnique.fr Thu Nov 15 15:38:52 2007 From: Lengrand at LIX.Polytechnique.fr (=?ISO-8859-1?Q?=22St=E9phane_Lengrand_=28Work=29=22?=) Date: Thu, 15 Nov 2007 20:38:52 +0000 Subject: [TYPES] Permutation of beta-redexes in lambda-calculus In-Reply-To: <473CAAA0.2050202@LIX.Polytechnique.fr> References: <473CAAA0.2050202@LIX.Polytechnique.fr> Message-ID: <473CAE5C.2090207@LIX.Polytechnique.fr> Dear all, I have recently found it necessary to prove the following theorem (by a series of adjournment properties), and was wondering if it rings a bell to anyone. Definition: Let gamma be a new reduction rule of lambda-calculus defined as (lambda x.M) ((lambda y.N) P) ---> (lambda y.(lambda x.M) N) P (avoiding capture of y in M, obviously) Theorem: If M is SN for beta, then M is SN for beta+gamma. The rule comes up in my framework for a call-by-value evaluation similar to Moggi's lambdaC. I'm sure that its termination (together with beta-reduction) must have already come up in someone else's work... Stephane Lengrand lengrand at lix.polytechnique.fr From eduardo at sol.lifia.info.unlp.edu.ar Thu Nov 15 18:48:23 2007 From: eduardo at sol.lifia.info.unlp.edu.ar (eduardo@sol.lifia.info.unlp.edu.ar) Date: Thu, 15 Nov 2007 20:48:23 -0300 Subject: [TYPES] Permutation of beta-redexes in lambda-calculus In-Reply-To: <473CAE5C.2090207@LIX.Polytechnique.fr> References: <473CAAA0.2050202@LIX.Polytechnique.fr> <473CAE5C.2090207@LIX.Polytechnique.fr> Message-ID: <20071115204823.8lam9grx8gk4gwk8@webmail.lifia.info.unlp.edu.ar> Hi St?phane, Although not exactly what you are looking for and at the risk that you may very well have heard of it already, I thought I might mention a "mirror image" notion of permutation to the one you suggest. Instead of permuting this configuration @ / \ @ / \ you permute this other one @ / \ @ / \ This has been developed by Laurent Regnier in 1990 [1]. He calls it \sigma reduction and is formulated as follows: ((\x.U) V) W --> (\x.(U W)) V (x\notin W) (\x.\y.U) V --> \y.(\x.U) V (y\notin V) He proves that all \sigma-equivalent terms have the same longest (beta) reduction to normal form. As a consequence \sigma-reduction is perpetual. Also, you get a result corresponding to your theorem as a corollary. Regards, E. [1] Regnier, 1990, Une ?quivalence sur les lambda-termes, paru dans TCS 126 (1994). Quoting "St?phane Lengrand (Work)" : > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear all, > > I have recently found it necessary to prove the following theorem (by a > series of adjournment properties), and was wondering if it rings a bell > to anyone. > > Definition: Let gamma be a new reduction rule of lambda-calculus defined as > (lambda x.M) ((lambda y.N) P) ---> (lambda y.(lambda x.M) N) P > (avoiding capture of y in M, obviously) > > Theorem: If M is SN for beta, then M is SN for beta+gamma. > > The rule comes up in my framework for a call-by-value evaluation similar > to Moggi's lambdaC. > I'm sure that its termination (together with beta-reduction) must have > already come up in someone else's work... > > Stephane Lengrand > lengrand at lix.polytechnique.fr > ---------------------------------------------------------------- Este mensaje ha sido enviado utilizando IMP desde LIFIA. From regnier at iml.univ-mrs.fr Fri Nov 16 10:33:02 2007 From: regnier at iml.univ-mrs.fr (Laurent Regnier) Date: Fri, 16 Nov 2007 16:33:02 +0100 Subject: [TYPES] Permutation of beta-redexes in lambda-calculus In-Reply-To: <20071115204823.8lam9grx8gk4gwk8@webmail.lifia.info.unlp.edu.ar> References: <473CAAA0.2050202@LIX.Polytechnique.fr> <473CAE5C.2090207@LIX.Polytechnique.fr> <20071115204823.8lam9grx8gk4gwk8@webmail.lifia.info.unlp.edu.ar> Message-ID: <18237.47150.689264.813246@gargle.gargle.HOWL> Hello, > This [notion of redex permutation] has been developed by > Laurent Regnier in 1990 [1]. He calls it \sigma reduction and is > formulated as follows: > > ((\x.U) V) W --> (\x.(U W)) V (x\notin W) > (\x.\y.U) V --> \y.(\x.U) V (y\notin V) Thanks to Eduardo for mentioning this work. I should say that other people had already some work on it, eg it is used (and maybe defined for the first time) in an 87 de Vrijer paper (Exactly estimating functionals and strong normalization). On the other hand I have never heard of the CBV version that St?phane proposes. Bests, Laurent From jbw at macs.hw.ac.uk Thu Nov 29 03:03:01 2007 From: jbw at macs.hw.ac.uk (Joe Wells) Date: Thu, 29 Nov 2007 08:03:01 +0000 Subject: [TYPES] Permutation of beta-redexes in lambda-calculus In-Reply-To: <473CAE5C.2090207@LIX.Polytechnique.fr> (=?utf-8?Q?=22St?= =?utf-8?Q?=C3=A9phane?= Lengrand"'s message of "Thu\, 15 Nov 2007 20\:38\:52 +0000") References: <473CAAA0.2050202@LIX.Polytechnique.fr> <473CAE5C.2090207@LIX.Polytechnique.fr> Message-ID: <86fxypcwcq.fsf@macs.hw.ac.uk> "St?phane Lengrand (Work)" writes: > I have recently found it necessary to prove the following theorem (by a > series of adjournment properties), and was wondering if it rings a bell > to anyone. > > Definition: Let gamma be a new reduction rule of lambda-calculus defined as > (lambda x.M) ((lambda y.N) P) ---> (lambda y.(lambda x.M) N) P > (avoiding capture of y in M, obviously) > > Theorem: If M is SN for beta, then M is SN for beta+gamma. Dear St?phane, A extremely similar theorem is proven in: A. J. Kfoury, J. B. Wells. New Notions of Reduction and Non-Semantic Proofs of ?-Strong Normalization in Typed ?-Calculi. LICS 1995. For discussion of and pointers to related work (the original ?reduction with memory? method from Klop's 1980 Ph.D. thesis, de Groote's similar method, Regnier's work, etc.), see also this technical report: A. J. Kfoury, J. B. Wells. Addendum to ?New Notions of Reduction and Non-Semantic Proofs of ?-Strong Normalization in Typed ?-Calculi?. Computer Science Department, Boston University, Technical Report 95-007, 1995. See also the general result in the following paper: F. D. Kamareddine. Postponement, Conservation and Preservation of Strong Normalisation for Generalised Reduction. Journal of Logic and Computation, 10(5), pp. 721-738, 2000. I hope these pointers are helpful. -- Joe Wells From hak at ilog.com Thu Nov 29 12:18:51 2007 From: hak at ilog.com (=?UTF-8?B?SGFzc2FuIEHDr3QtS2FjaQ==?=) Date: Thu, 29 Nov 2007 09:18:51 -0800 Subject: [TYPES] Permutation of beta-redexes in lambda-calculus In-Reply-To: <86fxypcwcq.fsf@macs.hw.ac.uk> References: <473CAAA0.2050202@LIX.Polytechnique.fr> <473CAE5C.2090207@LIX.Polytechnique.fr> <86fxypcwcq.fsf@macs.hw.ac.uk> Message-ID: <474EF47B.60208@ilog.com> Hello, Regarding the enclosed message, the following two references may also be relevant: 1. Hassan Ait-Kaci and Jacques Garrigue Label-selective lambda-calculus: Syntax and confluence Theoretical Computer Science, 151:353--383, 1995 URL: http://citeseer.ist.psu.edu/174691.html 2. Jacques Garrigue and Hassan Ait-Kaci The typed polymorphic label-lelective lambda calculus in Proc. 21st ACM Symp. on Principles of Programming Languages pp.35--47, ACM Press, 1994 URL: http://citeseer.ist.psu.edu/garrigue94typed.html Regards, -hak -- Hassan A?t-Kaci * ILOG, Inc. - Product Division R&D http://koala.ilog.fr/wiki/bin/view/Main/HassanAitKaci From Sam.Lindley at ed.ac.uk Fri Dec 7 12:27:22 2007 From: Sam.Lindley at ed.ac.uk (Sam Lindley) Date: Fri, 07 Dec 2007 17:27:22 +0000 Subject: [TYPES] Permutation of beta-redexes in lambda-calculus Message-ID: <4759827A.3060102@ed.ac.uk> St?phane Lengrand (Work) wrote: > Dear all, > > I have recently found it necessary to prove the following theorem (by > a series of adjournment properties), and was wondering if it rings a > bell to anyone. > > Definition: Let gamma be a new reduction rule of lambda-calculus > defined as (lambda x.M) ((lambda y.N) P) ---> (lambda y.(lambda x.M) > N) P (avoiding capture of y in M, obviously) > > Theorem: If M is SN for beta, then M is SN for beta+gamma. > > The rule comes up in my framework for a call-by-value evaluation > similar to Moggi's lambdaC. I'm sure that its termination (together > with beta-reduction) must have already come up in someone else's > work... I considered this problem in Section 3.2 of my thesis. http://www.era.lib.ed.ac.uk/handle/1842/778 Sam