From grust at in.tum.de Tue Jan 2 05:52:10 2007 From: grust at in.tum.de (Torsten Grust) Date: Tue, 2 Jan 2007 11:52:10 +0100 Subject: [TYPES/announce] PLAN-X 2007: Last Call for Participation Message-ID: Last Call for Participation P L A N - X 2 0 0 7 Programming Language Technologies for XML An ACM SIGPLAN Workshop collocated with POPL 2007 Nice, France -- January 20, 2007 www.plan-x-2007.org Please join us for PLAN-X 2007, the fifth workshop in the PLAN-X series, dedicated to the interaction and integration of programming language technology and the world of XML. The XML data model and its associated languages add interesting twists to programming language practice as well as theory. Just like its four predecessors, the PLAN-X 2007 workshop turns the spotlight on how programming language technology can embrace and explain streaming XML transformations, types for XPath and XML updates, web service contracts, tree patterns in XQuery, LINQ and XML Schema, and more. PLAN-X 2007 will feature eight talks, four system demonstrations, extensive opportunity for discussion, and a keynote address by Christoph Koch (U Saarland, Germany). PLAN-X 2007 will be held in the Plaza Hotel (Nice, France) all-day on Saturday, January 20, 2007, just after and collocated with POPL 2007, the ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (January 17-19, 2007). -- PROGRAM (Saturday, January 20, 2007) 09:00--10:00 Welcome Invited Talk by Christoph Koch (U Saarland, Germany) XPath Leashed 10:00--10:30 Coffee break 10:30--12:00 Session 1: Research Papers Streaming XML Transformations Using Term Rewriting (Alain Frisch, Keisuke Nakano) How to Recognise Different Kinds of Tree Patterns From Quite a Long Way Away (Jan Hidders, Philippe Michiels, Jerome Simeon, Roel Vercammen) Lux: A Lightweight, Statically Typed XML Update Language (James Cheney) 12:00--01:30 Workshop lunch (provided) 01:30--03:10 Session 2: Research Papers and Demo Presentations A Theory of Contracts for Web Services (Giuseppe Castagna, Nils Gesbert, Luca Padovani) XML Transformation Language Based on Monadic Second Order Logic (Kazuhiro Inaba, Haruo Hosoya) Demo: MTran: An XML Transformation Language Bases on Monadic Second Order Logic (Kazuhiro Inaba, Haruo Hosoya) Demo: XCentric: A Logic-Programming Language for XML Processing (Jorge Coelho, M?rio Florido) Demo: LINQ to XSD (Ralf L?mmel) Demo: GeLaBa: A Framework to Define Classes of XML Documents and to Automatically Derive Specialized Infrastructures (Benoit Pin, Georges Andr? Silber) 03:10--04:00 Interactive Demos and Coffee break 04:00--05:30 Session 3: Research Papers XPath Typing Using a Modal Logic with Converse for Finite Trees (Pierre Geneves, Nabil Layaida, Alan Schmitt) Deciding Equivalence of Top-Down XML Transformations in Polynomial Time (Sebastian Maneth, Helmut Seidl) A Logic Your Typechecker Can Count On: Unordered Tree Types in Practice (Nate Foster, Benjamin C. Pierce, Alan Schmitt) -- REGISTRATION PLAN-X 2007 is held in cooperation with POPL 2007. You can register for the workshop via the POPL 2007 registration process (online or offline). Please visit http://www.regmaster.com/conf/popl2007.html Registration rates are shown below. Note that you can upgrade an existing POPL 2007 registration to include PLAN-X 2007. Workshop-only registration is possible as well. ACM or SIGPLAN Member $89 Non-Member $99 Student $89 Your registration includes a copy of the PLAN-X 2007 informal proceedings, coffee breaks, and lunch. -- PLAN-X 2007 Workshop Chairs - General Chair - Program Chair Torsten Grust Giorgio Ghelli TU M?nchen U Pisa Munich, Germany Pisa, Italy grust at in.tum.de ghelli at di.unipi.it -- PLAN-X 2007 Program Committee - Michael Benedikt (Lucent, USA) - Daniela Florescu (Oracle, USA) - Alain Frisch (INRIA Rocquencourt, France) - Giorgio Ghelli, Chair (U Pisa, Italy) - Haruo Hosoya (U Tokyo, Japan) - Anders M?ller (U Aarhus, Denmark) - Mukund Raghavachari (IBM T.J. Watson Research Center, USA) - Alan Schmitt (INRIA Rh?ne-Alpes, France) - Sophie Tison (U Lille, France) - Philip Wadler (U Edinburgh, UK) From jonathan.cohen at anu.edu.au Thu Jan 4 06:26:57 2007 From: jonathan.cohen at anu.edu.au (Jon Cohen) Date: Thu, 4 Jan 2007 22:26:57 +1100 Subject: [TYPES/announce] USMC'07: Final call for talks and registration Message-ID: <57FC6FC3-34A2-41CC-86F3-1C71060CA147@anu.edu.au> FINAL CALL FOR TALKS AND REGISTRATION Universal Structures in Mathematics and Computing http://usmc07.rsise.anu.edu.au The Australian National University Canberra, Australia 5 - 7 February 2007 * Deadline for registration: 2nd February 2007 * Deadline for talk titles and abstracts submission: 19th January 2007 This workshop aims to bring together researchers working in category theory, universal algebra, logic and their applications to computer science in order to highlight recent advances in these fields and to facilitate dialogue between the different camps. Of particular interest is work which spans two or more of these areas. Keynote Speakers: * Brian Davey (La Trobe, Australia) * Rob Goldblatt (VUW, New Zealand) * Ross Street (Macquarie, Australia) * Glynn Winskel (Cambridge, UK) Please see the workshop website for futher details on registration, submission of talks, topics of interest and accommodation details. The workshop is sponsored by the Australian Mathematical Sciences Institute (AMSI) and National ICT Australia. From skalka at cs.uvm.edu Wed Jan 3 08:55:55 2007 From: skalka at cs.uvm.edu (Christian Skalka) Date: Wed, 03 Jan 2007 08:55:55 -0500 Subject: [TYPES/announce] PhD Position in Computer Science at UVM Message-ID: <004601c72f3e$e4b03720$2802a8c0@Pers> ================================= PhD POSITION IN COMPUTER SCIENCE FOUNDATIONS OF COMPUTER SECURITY The University of Vermont, USA ================================= Location: Department of Computer Science, The University of Vermont (UVM), Burlington, Vermont, USA. http://www.cs.uvm.edu http://www.uvm.edu http://www.ci.burlington.vt.us Description: We are seeking qualified applicants for doctoral research opportunities in the foundations of computer security. Our current research has two main thrusts. The first is type-and-effect analysis for enforcing temporal safety properties in software as a form of programming language based security. The second is the use of formalisms and programming logics to specify and implement distributed trust management (authorization) systems for applications such as web services. More information about these projects and associated publications is available online: http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-projects.html Research will be conducted in the context of larger projects being carried out by the Distributed Systems Group: http://www.cs.uvm.edu/research/distrsys This position is funded by a grant from the Department of Defense (DoD), Air Force Office of Scientific Research (AFOSR). Inquiries: Please direct questions to Christian Skalka, skalka at cs.uvm.edu, http://www.cs.uvm.edu/~skalka. To Apply: Information about the UVM Computer Science PhD Program, including information about applying, is available on the web: http://www.cs.uvm.edu/gradinfo/PhD-guide.shtml The deadline for applications to start in Fall 2007 is February 1, 2007. ============================== Christian Skalka Assistant Professor Department of Computer Science University of Vermont http://www.cs.uvm.edu/~skalka ============================== From Philippe.LAHIRE at unice.fr Wed Jan 3 13:03:44 2007 From: Philippe.LAHIRE at unice.fr (Philippe.LAHIRE@unice.fr) Date: Wed, 03 Jan 2007 19:03:44 +0100 Subject: [TYPES/announce] 29 days to go until TOOLS Europe submission deadline Message-ID: <459BF000.20005@unice.fr> ============================================================================ TOOLS EUROPE 2007 Objects, Models, Components, Patterns ETH Zurich, Switzerland 24-28 June 2007 http://tools.ethz.ch/ ============================================================================ Call for Papers TOOLS EUROPE 2007 will be devoted to the combination of technologies that have emerged as a result of object technology becoming "mainstream". Like its predecessors, TOOLS EUROPE 2007 combines an emphasis on quality with a strong practical focus. This is the 45th TOOLS conference. Started in 1989, TOOLS conferences, held in Europe, the USA, Australia, China and Eastern Europe, have played a major role in the development of object technology field; many of the seminal concepts were first presented at TOOLS. After an interruption of four years, the conference is now revived to reflect the maturing of the field and the new challenges ahead. Contributions are solicited on all aspects of object technology and neighbouring fields, in particular model-based development, component-based development, and patterns (design, analysis and other applications); more generally, any contribution addressing topics in advanced software technology fall within the scope of TOOLS. Reflecting the practical emphasis of TOOLS, contributions showcasing applications along with a sound conceptual contribution are particularly welcome. For a non-exclusive list of potential topic areas see the conference Web page. Submission Guidelines All contributions will be subject to a rigorous selection process by the international Program Committee, with a stress on originality, practicality and overall quality. Every paper will be reviewed by at least 4 committee members. The acceptance rate will be published in the conference proceedings; TOOLS is committed to a fair and extensive peer-review process establishing a high standard in the area of modern practices in software engineering. By submitting a paper to TOOLS, authors warrant that the work is original and that the paper or a similar contribution is neither published nor considered for publication elsewhere. Submissions should follow the publication format of the Journal of Object Technology (JOT). Papers should be limited in size to 20 single-spaced pages. Further details are available from the website. Important Dates Deadline for technical papers: February 1, 2007, midnight Zurich time Author notification: April 15, 2007 Camera-ready copy due: May 15, 2007 The proceedings will be published as a special issue of the Journal of Object Technology. TOOLS EUROPE will also include workshops and tutorials (June 24), a poster session, and a venture forum (June 28). See the corresponding calls for contributions. Chairpersons Conference chair: Bertrand Meyer Program chair: Jean Bezivin Publicity chairs: Philippe Lahire, Laurence Tratt Program committee Patrick Albert, Gustavo Alonso, Uwe Assman, Don Batory, Claude Baudoin, Bernhard Beckert, Jean-Pierre Briot, Stefano Ceri, Siobh?n Clarke, Pierre Cointe, Charles Consel, Bernard Coulette, Patrick Cousot, Krystof Czarnecki, Tharam Dillon, Klaus Dittrich, Gregor Engels, Jacky Estublier, Jose Fiadeiro, Judit Nyekyne Gaizler, Viktor Gergel, Carlo Ghezzi, Yossi Gil, Martin Gogolla, Jeff Gray, Rachid Guerraoui, Pedro Guerreiro, Alan Hartmann, Reiko Heckel, Connie Heitmeyer, Valerie Issarny, Gerti Kappel, Joseph Kiniry, Ivan Kurtev, Philippe Lahire, Ralf L?mmel, Gary Leavens, Rustan Leino, Mingshu Li, Tiziana Margaria, Erik Meijer, Silvio Meira, Christine Mingins, Peter M?ller, Elie Najm, Oscar Nierstrasz, Jonathan Ostroff, Richard Paige, Alfonso Pierantonio, Jaroslav Pokorny, Ralf Reussner, Richard Riehle, Nicolas Rouquette, Anthony Savidis, Doug Schmidt, Bran Selic, Richard Mark Soley, Clemens Szyperski, Dave Thomas, T.H. Tse, Antonio Vallecillo, Alan Cameron Wills, Amiram Yehudai From supratik at cc.usu.edu Thu Jan 4 18:49:15 2007 From: supratik at cc.usu.edu (supratik@cc.usu.edu) Date: Thu, 04 Jan 2007 16:49:15 -0700 Subject: [TYPES/announce] Call for Papers: AVIS 2007 Message-ID: <46119.1167954555@cc.usu.edu> An HTML attachment was scrubbed... URL: http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20070104/e58ac356/attachment.htm From Ricky.Robinson at nicta.com.au Thu Jan 4 20:40:15 2007 From: Ricky.Robinson at nicta.com.au (Ricky Robinson) Date: Fri, 5 Jan 2007 12:40:15 +1100 Subject: [TYPES/announce] DAIS 2007: Extended submission deadline Message-ID: <09D3F703EF3B0A4CBE28449EA9F3D32004B129C0@nicta-atp-mail.in.nicta.com.au> --------------------------------------------------------------------- Third CALL FOR PAPERS *EXTENDED SUBMISSION DEADLINE* DAIS 2007 7th IFIP International Conference on Distributed Applications and Interoperable Systems "Towards Sustainability" Paphos, Cyprus 6 - 8 June 2007 --------------------------------------------------------------------- Abstract submission: 15 January 2007 Paper submission: 22 January 2007 Work-in-progress papers: 2 February, 2007 Author notification: 7 March 2007 Camera-ready copy: 26 March 2007 --------------------------------------------------------------------- http://www.discotec07.cs.ucy.ac.cy --------------------------------------------------------------------- The 7th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS) is part of the federated conferences DisCoTec (Distributed Computing Techniques), together with the 9th International Conference on Coordination Models and Languages (COORDINATION) and the 9th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS). It will be organised by the Department of Computer Science of the University of Cyprus. ABOUT THE CONFERENCE Distributed applications and interoperable systems have become an integral part of everyday living, part of the socio-economic ecosystem of our human environment. With such interdependence between society and software, distributed software applications must be sustainable and adaptable in the long term, despite the changes in our environment. What do we understand by sustainability in distributed applications and interoperable systems? How do we ensure our distributed applications can make local adaptation to specific circumstances of their deployment? How do we make our interoperable systems evolvable in the face of widespread change in their environment? How do we integrate distributed software within the wider fabric of computing within our modern world? How can distributed applications and interoperable systems capitalise and exploit future trends and the changing user demographic? The DAIS conference series addresses all aspects of distributed applications and interoperable systems: design, implementation, operation and maintenance. This time we particularly solicit papers that address sustainability issues. DAIS'07 is the 7th event in this successful international conference series, commencing in 1997. It will be a forum for researchers, vendors and users to come together to review, discuss and learn about the future of distributed applications and interoperable systems. DAIS is now an annual event. CONFERENCE THEMES DAIS'07 solicits high quality papers reporting research results and/or experience reports. All papers must be original, unpublished and not submitted simultaneously for publication elsewhere. DAIS'07 conference themes include: - innovative distributed applications in the areas of * enterprise computing * mobile, grid and peer-to-peer computing * context-aware, ubiquitous and pervasive computing - models and concepts supporting distributed applications in the areas of * sustainability * adaptability * evolution - middleware supporting distributed applications in the area of * autonomic applications and systems * context-aware, adaptive applications * reconfigurable and self-managing applications * quality of service-aware applications - evolution of application integration and interoperability in * enterprise-wide and inter-enterprise integration * semantic interoperability and semantic web services * service-oriented applications - software engineering of distributed applications * domain-specific modeling languages * model evolution * model-driven adaptation, testing and validation * re-engineering SUBMISSION GUIDELINES Submissions must be done electronically as postscript or PDF, using the Springer LNCS style. DAIS'07 seeks: - Full technical papers in no more than 14 pages, - Work-in-progress papers, describing on-going work and interim results, in no more than 6 pages. Both categories of papers will be reviewed thoroughly by the DAIS'07 Program Committee. Accepted papers will appear in the conference proceedings published by Springer Verlag in the LNCS series. More specific guidelines on the preparation of papers can be found on the conference website. IMPORTANT DATES Abstract submission January 15, 2007 Full paper submission: January 22, 2007 Work-in-progress papers: February 2, 2007 Notification of acceptance: March 7, 2007 Camera ready version: March 26, 2007 ORGANISERS General chair: George Angelos Papadopoulos, University of Cyprus, Cyprus Steering committee: Lea Kutvonen, University of Helsinki, Finland Hartmut Koenig, BTU Cottbus, Germany Kurt Geihs, University of Kassel, Germany Elie Najm, ENST, Paris, France PC Chairs: Jadwiga Indulska, University of Queensland, Australia Kerry Raymond, Queensland University of Technology, Australia Publicity chair: Ricky Robinson, National ICT Australia, Australia Program committee: N. Alonistioti, University of Athens, Greece D. Bakken, Washington State University, USA Y. Berbers, Katholieke Universiteit Leuven, Belgium A. Beugnard, ENST-Bretagne, France G. Blair, Lancaster University, UK I. Demeure, ENST, France C. Eckert, TU Darmstadt, Germany F. Eliassen, University of Oslo, Norway P. Felber, Universit? de Neuch?tel, Switzerland, K. Geihs, University of Kassel, Germany R. Gr?nmo, SINTEF ICT, Norway D. Hagimont, INP Toulouse, France S. Hallsteinsen, SINTEF ICT, Norway J. Indulska, University of Queensland, Australia H. Koenig, BTU Cottbus, Germany R. Kroeger, Univeristy of Applied Sciences, Wiesbaden, Germany L. Kutvonen, University of Helsinki, Finland W. Lamersdorf, University of Hamburg, Germany M. Lawley, Queensland University of Technology, Australia P. Linington, University of Kent, UK C. Linnhof-Popien, University of Munich, Germany K. Lund, Norwegian Defence Research Establishment (FFI), Norway R. Meier, Trinity College Dublin, Ireland L. Merakos, University of Athens, Greece A. Montresor, University of Trento, Italy E. Najm, ENST, France R. Oliveira, Universidade do Minho, Portugal A. Puder State University San Francisco, USA K. Raymond, Queensland University of Technology, Australia R. Robinson, National ICT Australia, Australia A. Schill, Technical University of Dresden, Germany T. Senivongse, Chulalongkorn University, Thailand K. Sere, ?bo Akademi University, Finland J. B. Stefani, INRIA, France E. Tanter, University of Chile, Chile K. Zielinski, AGH Univ. of Science and Technology, Poland -- Ricky Robinson, Ph.D. Researcher Queensland Laboratory National ICT Australia Limited PO Box 10161 Brisbane QLD 4000 Australia Tel. +61 7 3000 0514 Fax. +61 7 3000 0480 The imagination driving Australia's ICT future. To receive the latest NICTA information register at http://nicta.com.au/registration.cfm -------------------------------------------------------------------------- This email and any attachments may be confidential. They may contain legally privileged information or copyright material. You should not read, copy, use or disclose them without authorisation. If you are not an intended recipient, please contact us at once by return email and then delete both messages. We do not accept liability in connection with computer virus, data corruption, delay, interruption, unauthorised access or unauthorised amendment. This notice should not be removed. From djg at cs.washington.edu Sat Jan 6 12:37:49 2007 From: djg at cs.washington.edu (Dan Grossman) Date: Sat, 06 Jan 2007 09:37:49 -0800 Subject: [TYPES/announce] Call-for-contributions: PASTE 2007 Message-ID: <459FDE6D.4000703@cs.washington.edu> [Research using types for software engineering would certainly fall under the scope of PASTE.] Of particular note are the "group presentations" which are a novel feature being tried at PASTE for the first time. --Dan ======= PASTE 2007 Call for Contributions 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering June 13-14, 2007 (co-located with PLDI 2007, part of FCRC 2007) http://paste07.cs.washington.edu/ PASTE is soliciting research papers and research-group presentations, each described in more detail below. PASTE 2007 is the seventh workshop in a series that brings together the program analysis, software tools, and software engineering communities to focus on applications of program analysis techniques in software tools. PASTE 2007 will provide a forum for the presentation of exciting research, empirical results, and new directions in areas including (but not limited to): * program analysis for program understanding, debugging, testing, and reverse engineering * integration of program analysis into programming environments * user interfaces for software tools and software visualization * applications of program slicing, model checking, and other program analysis techniques * analysis of program execution or program evolution * integration of, or tradeoffs between, different analysis techniques * issues in scaling analyses and user interfaces to deal with large systems PASTE will be a true workshop, with research presentations, organized discussions, an opportunity for all attendees to make short presentations, and ample time for debate. Research papers: We are soliciting short (6-page limit) research papers that describe ongoing research or new results. Papers should be formatted using the ACM SIG templates, and, including figures and references, should not exceed the page limit. Accepted papers will be published by ACM. The program committee will select papers based on technical quality, relevance to the PASTE community, and ability to inspire new research. Research-Group Presentations: We are soliciting group presentations describing a body of work relevant to PASTE. Groups should submit an overview of a one-hour presentation; this overview should not exceed 2 pages. A group presentation may describe past (retrospective), present (ongoing), or future (agenda) work or a combination thereof. One model we encourage is a short introduction by a faculty member followed by 3-4 student presentations that reinforce a theme. Selected presentations will have the option of including a 2-page abstract in the published proceedings. The program committee will select presentations based on relevance, timeliness, and a coherent theme. The committee will prefer presentations that will spark discussion and be accessible to the entire PASTE community. Because these presentations are new, we encourage interested groups to send questions and ideas to the co-chairs. Important dates: Submission deadline: Wednesday February 7, 2007, 11:59PM Samoan Time (firm) Author notification: Saturday March 10, 2007 Camera-ready copy due: April 2, 2007 Workshop: June 13-14, 2007 Program committee: Manuvir Das (co-chair) Microsoft Center for Software Excellence Harald Gall University of Zurich Dan Grossman (co-chair) University of Washington Laurie Hendren McGill University Ranjit Jhala University of California, San Diego Ben Liblit University of Wisconsin-Madison Gail Murphy University of British Columbia Radu Rugina Cornell University From leavens at cs.iastate.edu Sun Jan 7 20:36:27 2007 From: leavens at cs.iastate.edu (Gary T. Leavens) Date: Sun, 7 Jan 2007 19:36:27 -0600 (CST) Subject: [TYPES/announce] CFP: Foundations of Aspect-Oriented Languages FOAL 2007 Message-ID: [FOAL is very interested in papers on types and semantics related to aspect-oriented languages. Please contribute!] Call For Papers FOAL: Foundations of Aspect-Oriented Languages 2007 A one day workshop affiliated with AOSD 2007 in Vancouver, British Columbia. Submission Deadline: 23:00 GMT, 10 January 2007 Notification of Acceptance: 2 February 2007 Final Versions of Papers Due: 1 March 2007 Workshop: 13 March 2007 Themes and Goals FOAL is a forum for research in foundations of aspect-oriented programming languages. Areas of interest include but are not limited to: * Semantics of aspect-oriented languages * Specification and verification for such languages * Type systems * Static analysis * Theory of testing * Theory of aspect composition * Theory of aspect translation (compilation) and rewriting The workshop aims to foster work in foundations, including formal studies, promote the exchange of ideas, and encourage workers in the semantics and formal methods communities to do research in the area of aspect-oriented programming languages. All theoretical and foundational studies of this topic are welcome. The goals of FOAL are to: * Make progress on the foundations of aspect-oriented programming languages. * Exchange ideas about semantics and formal methods for aspect-oriented programming languages. * Foster interest within the programming language theory and types communities in aspect-oriented programming languages. * Foster interest within the formal methods community in aspect-oriented programming and the problems of reasoning about aspect-oriented programs. Workshop Format The planned workshop format is primarily presentation of papers and group discussion. Talks will come in three categories: long (30 minutes plus 15 minutes of discussion), regular (20 minutes plus 5 minutes of discussion) and short (7 minutes plus 3 minutes of discussion). The short talks will allow for presentations of topics for which results are not yet available, perhaps for researchers who are seeking feedback on ideas or seek collaborations. We also plan to ensure sufficient time for discussion of each presentation by limiting the overall number of talks. Submissions Invitation to the workshop will be based on papers selected by the program committee; those wishing to attend but not having a paper to submit should contact the organizers directly to see if there is sufficient space in the workshop. FOAL solicits long, regular, and short papers on all areas of formal foundations of AOP languages. Submissions will be read by the program committee and designated reviewers. Papers will be selected for long, regular, and short presentation at the workshop based on their length, scientific merit, innovation, readability, and relevance. Papers previously published or already being reviewed by another conference are not eligible. Some papers may not be selected for presentation, and some may be selected for presentation in shorter talks than their paper length would otherwise command. We will limit the length of paper presentations and the number of papers presented to make sure that there is enough time for discussion. Papers presented at the workshop will be included in a technical report (from Iowa State University). Authors will retain their own copyright to the papers. Publication of papers at other venues will thus remain possible. We will also investigate having a special issue of a journal for revisions of selected papers after the workshop. Authors should note the following details: * Submissions are due no later than 23:00 GMT, 10 January 2007. (This is a firm deadline.) * Authors must indicate whether they wish to be considered for a long, regular, or short presentation. * Papers for long presentations must not exceed 10 pages in length; those for regular presentations must not exceed 7 pages in length, and those for short presentations must not exceed 3 pages in length. * Some papers may not be selected for presentation, and some may be selected for presentation in shorter talks than requested. * We encourage use of the ACM Conference format for submissions, as this will be required for accepted papers. You must add page numbers (which are not part of the standard format) to your submissions, to make adding comments easier. * Submissions are to be made to the following URL: http://continue.cs.brown.edu/servlets/foal07/continue.ss We will notify the corresponding author of papers that are selected for presentation at the workshop by 2 February 2007. Early registration for AOSD (you must register for AOSD to attend the workshop) is 9 February 2007. Final versions of papers for the proceedings will be due on 1 March 2007. Important Dates Submission Deadline: 23:00 GMT, 10 January 2007 Notification of Acceptance: 2 February 2007 Final Versions of Papers Due: 1 March 2007 Workshop: 13 March 2007 For more information, visit the FOAL Workshop home page (at http://www.cs.iastate.edu/FOAL). Gary T. Leavens Department of Computer Science, Iowa State University 229 Atanasoff Hall, Ames, Iowa 50011-1041 USA http://www.cs.iastate.edu/~leavens phone: +1-515-294-1580 From Sukyoung.Ryu at sun.com Tue Jan 9 11:51:30 2007 From: Sukyoung.Ryu at sun.com (Sukyoung Ryu) Date: Tue, 09 Jan 2007 11:51:30 -0500 Subject: [TYPES/announce] Announcement: A reference implementation of Fortress Message-ID: <15BAD214-C408-47CE-8A0E-A962DEC60DD8@sun.com> We'd like to announce availability of a preliminary, open source, interpreter implementing a small core of the Fortress programming language. This interpreter runs on the JVM. You can download the source code at: http://fortress.sunsource.net/ Our intention is to grow this implementation over time, with the help of university partners and other interested third parties. We expect that many parts of this interpreter will be used as components of a complete Fortress compiler, which is our long term goal. Fortress is a new programming language designed for high-performance computing (HPC) with high programmability. In order to explore breakaway approaches to improving programmability, the Fortress design has not been tied to legacy language syntax or semantics; all aspects of HPC language design have been rethought from the ground up. As a result, we are able to support features in Fortress such as transactions, specification of locality, and implicit parallel computation, as integral features built into the core of the language. Features such as the Fortress component system and test framework facilitate program assembly and testing, and enable powerful compiler optimizations across library boundaries. Even the syntax and type system of Fortress are custom-tailored to modern HPC programming, supporting mathematical notation and static checking of properties such as physical units and dimensions, static type checking of multidimensional arrays and matrices, and definitions of domain-specific language syntax in libraries. Moreover, Fortress has been designed with the intent that it be a "growable" language, gracefully supporting the addition of future language features. In fact, much of the Fortress language itself (even the definition of arrays and other basic types) is encoded in libraries atop a relatively small core language. For further information and downloads, please visit: http://fortress.sunsource.net/ Comments and feedback are welcome. ====================================================================== Programming Language Research Group, Sun Microsystems Laboratories From finco07 at cs.brown.edu Tue Jan 9 22:03:09 2007 From: finco07 at cs.brown.edu (FINCO 2007) Date: Tue, 9 Jan 2007 22:03:09 -0500 Subject: [TYPES/announce] CFP: Foundations of Interactive Computation In-Reply-To: References: Message-ID: call for papers FInCo 2007: FOUNDATIONS OF INTERACTIVE COMPUTATION satellite workshop of ETAPS 2007 Saturday 31 March 2007, Braga, Portugal http://www.cs.brown.edu/sites/finco07 ==================================================== The interaction paradigm provides a new conceptualization of compu- tational phenomena, placing the emphasis on interaction rather than on algorithms; concurrent, distributed, reactive, embedded, component- oriented, agent-oriented and service-oriented systems all exploit interaction as a fundamental paradigm. Contemporary approaches to Software Engineering, Artificial Intelligence, Programming Languages, and Networking are all part of this paradigm change. However, a satis- factory unified foundational framework for interactive computation is still lacking, analogous to the one that Turing Machines and lambda- calculus provide for algorithms. Following the success of FInCo 2005, this workshop provides an opportunity for researchers to meet and ex- change ideas, with the ultimate goal of providing a unified conceptual and formal framework for interactive computation. The following characteristics distinguish this new, interactive notion of computation: Computational Problem: The notion of a computational problem includes performing a task or providing a service, rather than being rest- ricted to algorithmically producing an answer to a question. Observable Behavior: A computing component is modeled in terms of its observable behavior, where later input values may depend on earlier output values and vice versa. Environments: The world, or environment of the computation is part of the model, dynamically supplying the computational system with the inputs, and consuming the output values from the system. Concurrency: Computation may be concurrent, where the computing agent computes in parallel with its environment, and with other agents in it. The claim that "interaction is more powerful than algorithms" is an open invitation to researchers to develop the tools and methods that can lend credence to this claim. Many models capturing different aspects of interaction have been introduced, including interaction automata and process algebras. It is now time for researchers involved in interactive systems to join their efforts and collaborate to develop a common frame- work that focuses on constructive models of computation that exploit interaction as a first-class concept. Accordingly, FInCo 2007 has the following goals: * Understand the fundamental issues underlying the interaction paradigm; * Establish a common language- and domain-independent framework for a theory of interactive computation; * Identify the interactive principles of effective and reliable engi- neering of software systems; * Map out the design space of models of interaction, towards accompli- shing above goals. WORKSHOP PANEL Title: Interactive Models for Software Engineering Moderator: Peter Wegner, Brown University, USA Description: Software & systems engineering of today is being affected by the growing importance of interaction. This panel considers the role of interaction in the theory and practice of computing, with a special focus on system design and development. PAPERS We solicit papers addressing one or more of the above goals. Submit papers by email to by Jan. 31, 2007, with a 12- page limit. Workshop proceedings will be published by ENTCS. Selected papers will be invited for journal publication. For a PDF copy of this announcement, and for further information, see our web site at http://www.cs.brown.edu/sites/finco07 IMPORTANT DATES Submission: Jan. 31, 2007 Notification: Feb. 28, 2007 Workshop: Mar. 31, 2007 ORGANIZERS Farhad Arbab, CWI and Leiden Univ., The Netherlands Dina Goldin, Brown Univ., USA (chair) PROGRAM COMMITTEE Gul Agha, UIUC, USA Luca de Alfaro, UC Santa Cruz, USA Luis Barbosa, Univ. do Minho, Portugal Antonio Brogi, Univ. di Pisa, Italy Jon Doyle, North Carolina State U., USA Giorgio Delzanno, Univ. di Genova, Italy Jos? Luiz Fiadeiro, Univ. of Leicester, UK Rob van Glabbeek, Univ. of New South Wales, Australia Kees van Hee, Technische Univ. Eindhoven, The Netherlands Orna Kupferman, Hebrew Univ., Israel R. Prescott Loui, Washington Univ. in St. Louis, USA Peter McBurney, Univ. of Liverpool, UK John-Jules Meyer, Utrecht Univ., the Netherlands Ugo Montanari, Univ. di Pisa, Italy Rocco De Nicola, Univ. degli Studi di Firenze, Italy Andrea Omicini, Univ. di Bologna - Cesena, Italy Catuscia Palamidessi, INRIA and LIX ?cole Polytechnique, France Jean-Eric Pin, Univ. Paris Denis Diderot and CNRS, France Vladimiro Sassone, Univ. of Sussex, UK Douglas C. Schmidt, Vanderbilt Univ., USA Carolyn Talcott, SRI Int'l, USA Bernhard Thalheim, Kiel Univ., Germany STEERING COMMITTEE Manfred Broy, TU M?nchen, Germany Dina Goldin, Brown Univ., USA Mirko Viroli, Univ. Bologna/Cesena, Italy Peter Wegner, Brown Univ., USA WEB SITE http://www.cs.brown.edu/sites/finco07 From streicher at mathematik.tu-darmstadt.de Thu Jan 11 05:54:54 2007 From: streicher at mathematik.tu-darmstadt.de (Thomas Streicher) Date: Thu, 11 Jan 2007 11:54:54 +0100 (CET) Subject: [TYPES/announce] Workshop announcement (Domains VIII) Message-ID: <200701111054.l0BAssE9017449@fb04209.mathematik.tu-darmstadt.de> This announcement is also attached as a pdf-file Announcement and Call for Abstracts Joint Workshop Domains VIII and Computability Over Continuous Data Types Novosibirsk, September 11 -- 15, 2007 The Workshop 'Domains' series is aimed at computer scientists and mathematicians alike who share an interest in the mathematical foundations of computation. It focusses on domain theory, its applications and related topics. It will be combined with topics based on the German--Russian project 'Computability Over Non-discrete Structures: Models, Semantics, Complexity' supported by Russian Foundation for Basic Research (RFBR) and Deutsche Forschungsgemeinschaft (DFG). Webpage: www.sbras.ru/ws/domains/ (Switch to English - upper right corner) email: domains at math.nsc.ru SCOPE Topics for this workshop include, but are not limited to domains and topology for semantics effective domains and spaces computation over continuous spaces program semantics models of sequential computation lambda calculus realizability proof mining constructive mathematics and its semantics computability theory computable models admissible sets LOCATION The Workshop will take place at the Sobolev Instituts of Mathematics of the Siberian Branch of the Russian Academy of Sciences located in Akademgorodok, which is formally a district of Novosibirsk. PARTICIPATION If you would like to participate in this workshop, please let us know your interest at an early stage. Please indicate whether you intend to give a talk: domains at math.nsc.ru SUBMISSION OF ABSTRACTS One page abstracts should be submitted to domains at math.nsc.ru Shortly after an abstract is submitted (usually a few weeks), the authors will be notified by the programme committee. Abstracts will be dealt with on a first come/first served basis. Submit as soon as possible. DEADLINE 15 May 2007\\[2mm] INVITED SPEAKERS will be announced later on. PROCEEDINGS Conference Proceedings will be published in a Journal. Submission for the Proceddings will be after the Workshop. They will be refereed according to the usual requirements of the Journal. ACCOMODATION All participants will be accommodated in the Hotel ``Zolotaya Dolina'' (Gold Valley) situated at walking distance from the Instituts of Mathematics. FEES There will be a registration fee of 85 Euros for covering expenses. For participants from Eastern Europa and the former Soviet Union we set the fee 300 Russian Roubles. PhD students do not pay a fee. If the fee is a problem, please contact the organizers for a possible arrangement in advance. VISAS AND REGISTRATION Most foreign participants will need a visa to enter Russia. We will inform you later about details. You also can find details at http://www.ict.nsc.ru/ws/ALC-9/visa.htm For obtaining a visa, one needs an official invitation issued by the local authorities at Novosibirsk. The processing of invitations takes about one month; in addition, please allow some time for sending it by mail!} DEADLINE for registration: 30 June, 2007 PROGRAMME COMMITTEE Yuri Ershov Sobolev Institute of Mathematics, Novosibirsk Sergei Goncharov Sobolev Institute of Mathematics, Novosibirsk Achim Jung University of Birmingham, Birmingham Klaus Keimel (Chair) Darmstadt Technical University, Darmstadt Ulrich Kohlenbach Darmstadt Technical University, Darmstadt Andrei Morozov (Co-Chair) Sobolev Institute of Mathematics, Novosibirsk Victor Selivanov Novosibirsk State Pedagogical University, Novosibirsk Dieter Spreen University of Siegen, Siegen WORKSHOP SECRETARY Alexei Stukachev (domains at math.nsc.ru) -------------- next part -------------- A non-text attachment was scrubbed... Name: announcement.pdf Type: application/octet-stream Size: 50821 bytes Desc: Url : http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20070111/08564d85/announcement.bin From dmitry.sustretov at loria.fr Fri Jan 12 08:32:08 2007 From: dmitry.sustretov at loria.fr (Dmitry Sustretov) Date: Fri, 12 Jan 2007 14:32:08 +0100 Subject: [TYPES/announce] ESSLLI 2007 Student Session Final Call For Papers Message-ID: [Our apologies for multiple postings of this announcement.] ESSLLI 2007 STUDENT SESSION FINAL CALL FOR PAPERS August 6-17 2007, Dublin, Ireland Deadline: February 11, 2007 http://www.loria.fr/~sustreto/stus07/ We are pleased to announce the Student Session of the 19th European Summer School in Logic, Language and Information, which will be held in Dublin, Ireland on August 6-17, 2007. We invite submission of papers in the areas of Logic, Language and Computation for presentation at the Student Session and for appearance in the proceedings. AIM Student Session exists to bring together young researchers to present and discuss their work in progress with a possibility to get feedback from senior researchers. SUBMISSION Only original publications are accepted, previous published works are not allowed. All authors of the paper must be students: undergraduate (before the completion of the Masters degree) or graduate (before the completion of the PhD degree). Papers can be submitted either for oral (20min talk+10 min discussion), or poster presentation. There are three subject areas: Logic and Language (lola), Language and Computation (laco) and Logic and Computation (loco). The submissions should be sent by email before 11 February 2007 to dmitry.sustretov at loria.fr (the message should have subject "ESSLLI STUS submission") along with an identification file in plain text of the following format: Title: title of the submission First author: firstname lastname Affiliation: affiliation of the first author E-mail: e-mail of the first author ...... Last author: firstname lastname Affiliation: affiliation of the last author E-mail: e-mail of the last author Abstract: (5 lines) Subject area: Logic and Language or Language and Computation or Logic and Computation Modality: Poster or Oral The submission should be in one of the following formats: PostScript, PDF or RTF. (In case of acceptance, the final version of the paper will have to be submitted in LaTeX format.) The papers must use single column A4 size pages, 11pt or 12pt fonts, and standard margins, and may not exceed 7 pages of length exclusive of references. The paper and identification file should be named by the following convention: category-modality-last name(s) of author(s) (for example, "loco-oral-martin.pdf" and "loco-oral-martin.txt"). At least one of the authors of the paper must register as a participant of ESSLLI. Accepted papers will be published in the proceedings which will be available during ESSLLI. TIMELINE Submission deadline: February 11, 2007 Notification of authors: April 20, 2007 Full paper deadline: May 20, 2007 ESSLLI: August 6-17, 2007 PROGRAM COMMITTEE Chairs: Ville Nurmi, University of Helsinki Dmitry Sustretov, LORIA Area experts: Paul Buitelaar (Language & Computation) Valentin Goranko (Logic & Computation) Carl Pollard (Logic & Language) Co-chairs: Logic & Computation Bryan Renne, City University of New York Levan Uridia, University of Amsterdam Language & Computation Luciana Benotti, INRIA Lorraine Michael Kaisser, University of Edinburgh Logic & Language Jana H?ussler, University of Konstanz Miltiadis Kokkonidis, University of Oxford CONTACT The Student Session webpage is the place for relevant information. http://www.loria.fr/~sustreto/stus07/ Feel free to contact the chairs for any questions about the submissions or the Student Session in general. Ville Nurmi Phone: +358 9 191 51497 Fax: +358 9 191 51400 E-mail: ville.v.nurmi at helsinki.fi Dmitry Sustretov Phone: +33 3 83 59 20 35 Fax: +33 3 83 41 30 79 E-mail: dmitry.sustretov at loria.fr From aichernig at ist.tugraz.at Fri Jan 12 12:55:52 2007 From: aichernig at ist.tugraz.at (Bernhard K. Aichernig) Date: Fri, 12 Jan 2007 18:55:52 +0100 Subject: [TYPES/announce] ICTAC 2007: Call for Papers Message-ID: <1168624552.5024.188.camel@localhost.localdomain> Call for Papers ICTAC 2007 4th International Colloquium on Theoretical Aspects of Computing 26-28 September 2007, Macao SAR, China http://www.iist.unu.edu/ictac07 Important Dates: Paper submission: 20 April 2007, Notification of acceptance: 1 June 2007, Final copy for proceedings: 22 June 2007, ICTAC 2007: 26-28 September 2007. Associated Events: - School on Domain Modelling and the Duration Calculus, 17-21 September 2007, Shanghai - Festschrift Symposium dedicated to the 70th birthdays of Dines Bj?rner and Zhou Chaochen, 24-25 September 2007, Macao - Workshops, 22-23 September, 2007, Macao See Call for Workshop Proposals at conference URL! ICTAC is an International Colloquium on Theoretical Aspects of Computing founded by the International Institute for Software Technology of the United Nations University (UNU-IIST). The aim of the colloquium is to bring together practitioners and researchers from academia, industry and government to present research results, and exchange experience, ideas, and solutions for their problems in theoretical aspects of computing. Beyond these scholarly goals, another main purpose of the conference is to promote cooperation in research and education between participants and their institutions, from developing and industrial countries, as in the mandate of the United Nations University. The previous three ICTAC events were held in Guiyang, China (2004), Hanoi, Vietnam (2005), Tunis, Tunisia (2006). The topics of the conference include, but are not limited to: - automata theory and formal languages - principles and semantics of programming languages - logics and their applications - software architectures and their description languages - software specification, refinement, and verification - model checking and theorem proving - formal techniques in software testing - models of object and component systems - coordination and feature interaction - integration of formal and engineering methods - service-oriented development - models of concurrency, security, and mobility - theory of parallel, distributed, and internet-based (grid) computing - real-time, embedded and hybrid systems - type and category theory in computer science - case studies - theories, tools and experiments of verified systems - integration of theories of system development and their tool support ICTAC 2007 will have a technical program for five days including a two-day festschrift symposium dedicated to the 70th birthdays of former UNU-IIST directors, Dines Bj?rner and Zhou Chaochen, and three days for a conference. There will also be a training school in the preceding week on topics of Domain Modelling and the Duration Calculus, to which Dines Bj?rner and Zhou Chaochen have made significant contribution. Paper Submissions: Submissions to the conference must not have been published or be concurrently considered for publication elsewhere. All submissions will be judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the conference. Papers should be written in English and not exceed 15 pages in LNCS format (see http://www.springer.de/comp/lncs/authors.html for details). Proceedings of the previous editions of ICTAC were published by Springer in the LNCS series. We plan to do the same this year. Best papers will be selected from the accepted papers and their authors invited to submit an extended version of their work to a special issue of Formal Aspects of Computing. Submission Procedure: Further information and instruction about submission can be found at the conference website http://www.iist.unu.edu/ictac07. General Chairs: John Fitzgerald, Newcastle University, UK George Michael Reed, UNU-IIST, Macao Program Chairs: Cliff Jones, Newcastle University, UK Zhiming Liu, UNU-IIST, Macao Jim Woodcock, University of York, UK Organisation Co-Chairs: Chris George, UNU-IIST, Macao Workshop Chair: Dang Van Hung, UNU-IIST, Macao Publicity Chair: Bernhard K. Aichernig, TU Graz, Austria Sponsored by: UNU-IIST, Formal Methods Europe PC Members: M?che?l mac an Airchinnigh, IE Farhad.Arbab, NL Kamel Barkaoui, FR Jonathan P. Bowen, UK Andrew Butterfield, IE Ana Cavalcanti, UK Antonio Cerone, MO Jim Davies, UK David Deharbe, BR Jin Song Dong, SG Lindsay Groves, NZ Stefan Hallerstede, CH Michael Hansen, DK Ian Hayes, AU Dang Van Hung, MO Mathai Joseph, IN Joseph Kiniry, IE Peter Gorm Larsen,DK Xuandong Li, CN Shaoying Liu, JP Ali Mili, US Joe Morris, IE Leonor Prensa Nieto, FR Anders Ravn, DK Augusto Sampaio, BR Emil Sekerinski, CA Natarajan Shankar, US Ji Wang, CN Naijun Zhan, CN Invited Speakers: TBA -- Dr. Bernhard K. Aichernig, Assistant Professor, IST, TU Graz http://www.ist.tugraz.at/aichernig From bpientka at cs.mcgill.ca Mon Jan 15 21:08:05 2007 From: bpientka at cs.mcgill.ca (Brigitte Pientka) Date: Mon, 15 Jan 2007 21:08:05 -0500 (EST) Subject: [TYPES/announce] LFMTP'07: Call for papers Message-ID: ----------------------------------------------------------------------- International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'07) http://www.cs.mcgill.ca/~bpientka/lfmtp07 Affiliated with CADE-21 Bremen, Germany, 16 July, 2007 CALL FOR PAPERS Important Dates: Abstract Submission 7 May 2007 Submission deadline: 13 May 2007 Author Notification: 3 June 2007 Final Version: 17 June 2007 Workshop day 16 July ----------------------------------------------------------------------- LFMTP'07 continues the International workshop on Logical Frameworks and Meta-languages (LFM) and the MERLIN workshop on MEchanized Reasoning about Languages with variable BIndingIN). Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation on the one hand and their applications in for example proof-carrying code have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss all aspects of logical frameworks. The broad subject areas of LFMTP'07 are * The automation and implementation of the meta-theory of programming languages and related calculi, particularly work which involves variable binding and fresh name generation. * The theoretical and practical issues concerning the encoding of variable binding and fresh name generation, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Case studies of meta-programming, and the mechanization of the (meta)theory of descriptions of programming languages and other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory are particularly welcome. Topics include, but are not limited to * logical framework design * meta-theoretic analysis * applications and comparative studies * implementation techniques * efficient proof representation and validation * proof-generating decision procedures and theorem provers * proof-carrying code * substructural frameworks * semantic foundations * methods for reasoning about logics * formal digital libraries Invited Speaker: to be announced Program Committee: Andreas Abel (LMU Munich) Peter Dybjer (Chalmers University) Marino Miculan (University Udine) Dale Miller (INRIA Futurs) Brigitte Pientka (McGill University) Benjamin Pierce (University of Pennsylvania) Carsten Schuermann (IT University of Copenhagen, PC Chair) Christian Urban (TU Munich) Paper Submissions: Three categories of papers are solicited: * Category A: Detailed and technical accounts of new research: up to fifteen pages including bibliography. * Category B: Shorter accounts of work in progress and proposed further directions, including discussion papers: up to eight pages including bibliography and appendices. * Category C: System descriptions presenting an implemented tool and its novel features: up to six pages. A demonstration is expected to accompany the presentation. Submission is electronic in postscript or PDF format. Submitted papers must conform to the ENTCS style preferrably using LaTeX2e. For further information and submission instructions, see the LFMTP web page: http://www.cs.mcgill.ca/~bpientka/lfmtp07/index.html Proceedings are to be published as a volume in the Electronic Notes in Theoretical Computer Science (ENTCS) series and will be available to participants at the workshop. Authors of accepted papers are expected to present their paper at the workshop. Organizers: Brigitte Pientka Carsten Schuermann bpientka at cs.mcgill.ca carsten at itu.dk School of Computer Science Department of Theoretical Computer Science McGill University IT University of Copenhagen From andrei at cs.chalmers.se Tue Jan 16 04:16:40 2007 From: andrei at cs.chalmers.se (Andrei Sabelfeld) Date: Tue, 16 Jan 2007 10:16:40 +0100 (MET) Subject: [TYPES/announce] IEEE Computer Security Foundations Symposium 2007 - CFP Message-ID: <20070116091640.1734F31EC@zsh.cs.chalmers.se> A non-text attachment was scrubbed... Name: not available Type: text Size: 6753 bytes Desc: not available Url : http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20070116/48fed13b/attachment.txt From H.Geuvers at cs.ru.nl Tue Jan 16 10:06:07 2007 From: H.Geuvers at cs.ru.nl (Herman Geuvers) Date: Tue, 16 Jan 2007 16:06:07 +0100 Subject: [TYPES/announce] Call for Papers: RDP Workshop PATE Message-ID: <45ACE9DF.9090300@cs.ru.nl> ===================================================================== Call for Papers RDP 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 March 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 pierre.courtieu at gmail.com Tue Jan 16 11:48:45 2007 From: pierre.courtieu at gmail.com (Pierre Courtieu) Date: Tue, 16 Jan 2007 17:48:45 +0100 Subject: [TYPES/announce] CFP RDP Workshop Proof Assistants and Types in Education Message-ID: <20070116174845.72b09ea5@centaur.cnam.fr> ===================================================================== Call for Papers RDP 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 March 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 jbw at macs.hw.ac.uk Tue Jan 16 17:14:58 2007 From: jbw at macs.hw.ac.uk (Joe Wells) Date: Tue, 16 Jan 2007 22:14:58 +0000 Subject: [TYPES/announce] Research Job: Compositional Analysis for Mobility & Concurrency @ Heriot-Watt U., Scotland, UK Message-ID: <86k5zmvct9.fsf@macs.hw.ac.uk> Research Position ULTRA group (Useful Logics, Types, Rewriting, and their Automation) Computer Science Department School of Mathematical and Computer Sciences Heriot-Watt University Edinburgh, Scotland, UK The HTML version of this job posting can be found at: http://www.macs.hw.ac.uk/~jbw/position-ad.html Description of the Position A research position is available working on modular reasoning and compositional analysis for computer systems and software with special interest in mobility and concurrency. The position is working with Joe Wells[1] in the ULTRA (Useful Logics, Types, Rewriting, and their Automation) group[2] in the Computer Science Department[3] in the School of Mathematical and Computer Sciences[4] at Heriot-Watt University[5] in Edinburgh[6], the capital of Scotland[7]. The position involves collaboration with the EPSRC and NSF-funded Church Project[8] as well as various contacts in the European Global Computing community. The research will include collaboration on the Poly*[9] polymorphic retargetable type system for process and mobility calculi, but is not limited to that topic. It will be helpful if the researcher is competent in 1 or more of the following knowledge areas. * Formal calculi for reasoning about the meaning of computer systems (including computer programs), especially those dealing with aspects of (a) concurrency and (b) mobility, but also those dealing with aspects of (c) modules, linking, and loading, (d) resource usage, (e) components, (f) staged compilation, (g) classes and objects, etc. * Analysis of systems represented in formal calculi. * Constraint solving and unification. * Type systems, especially those with features similar to intersection and union types. * Programming languages good for use for any of the above. The duration of the position is 1.5 years, with possible further extension depending on performance, funding, and other circumstances. Applications to spend a shorter period (e.g., the sabbatical leave of an established academic) will be considered. The initial salary will be in the range from 22111 GBP to 32471 GBP per year, commensurate with qualifications and experience. The position is available immediately. It is preferred that before starting the researcher will have completed a Ph.D. in a relevant discipline in Computer Science. Very good Ph.D. students elsewhere who want to spend part of their studies visiting Heriot-Watt will be considered. Applicants from outside the European Economic Area (EEA) will be considered. The researcher will probably collaborate on 1 or more of the following activities. The specific activities will be matched to the strengths of the researcher. * Designing new type systems for compositional (modular) analysis of systems that may involve one or more aspects of mobility, concurrency, and modularity, as well as other features such as resource awareness, components, run-time code generation, objects, etc. * Designing analysis algorithms for the new type systems. * Designing theories (e.g., "calculi") for reasoning about the meaning of computer systems with some of the features mentioned above. * Making software systems incorporating the new type systems, algorithms, and calculi. * Writing scientific reports on the work done. References 1. http://www.macs.hw.ac.uk/~jbw/ 2. http://www.macs.hw.ac.uk/ultra/ 3. http://www.macs.hw.ac.uk/cs/ 4. http://www.macs.hw.ac.uk/ 5. http://www.hw.ac.uk/ 6. http://www.geo.ed.ac.uk/home/tour/edintour.html 7. http://www.geo.ed.ac.uk/home/scotland/scotland.html 8. http://www.church-project.org/ 9. http://www.macs.hw.ac.uk/DART/software/PolyStar/FAQ.html Contact Information Informal inquiries should be directed to Joe Wells at: Web: http://www.macs.hw.ac.uk/~jbw/ E-mail: jbw at macs.hw.ac.uk Fax: +44 131 451 3327 Formal applications should be directed to the Heriot-Watt Human Resources Office at: Web: http://www.hw.ac.uk/hr/ E-mail: hr at hw.ac.uk (responses will usually be by paper mail, telephone, or fax) Voice mail: +44 131 451 3475 (available at all times) Fax: +44 131 451 3475 Minicom: +44 131 451 8212 Post: Human Resources Office Heriot-Watt University EDINBURGH EH14 4AS GREAT BRITAIN Applying for the Position Please use the reference code 16/07/L to help prevent your application from getting mixed up. For documents sent by e-mail, please use a public and standard format. (The best formats are plain text and PDF, because some of our staff may have trouble with HTML or PostScript. Microsoft Word format is forbidden except where returning a form our human resources office has supplied in this format.) To formally apply for this position, please do as many as possible of the items in the following list by 2007-02-12. The first 2 items are absolutely necessary and the 3rd and 4th are quite important. If you expect trouble meeting the deadline, please ask Joe Wells what to do. * Cause 3 recommendation letters to be sent directly by their writers. Do not send the letters with your application. (If someone tells you the letters are not needed yet or that less than 3 are needed, this is a mistake. We want to see the letters before choosing who to interview.) * Send the following yourself: + your complete curriculum vitae, and + contact details for the 3 people writing your recommendation letters. * Get the Heriot-Watt Human Resources Office to send you an "application pack". (This contains an application form (available at http://www.hw.ac.uk/hr/htm/forms/Academic%20Application%20form.pdf), an equal opportunities monitoring form (available at http://www.hw.ac.uk/hr/htm/forms/Equal%20Opportunities%20Monitoring%20Form%20new%20Riccarton.doc), information for applicants with disabilities, and some additional information about Heriot-Watt and the position.) * Fill out and return by post the application form and the equal opportunities monitoring form. If your curriculum vitae is well constructed, then some information requested will be redundant, so just write "see c.v." in those blanks, but please return the application form anyway. Although the application form requests only the addresses of 2 references, please follow the instructions above instead and supply 3. * Optionally, also send either of the following: + a brief statement about why your research accomplishments and interests are a good match for the position, and + up to 3 relevant publications of yours. * It is helpful to inform Joe Wells that you are applying so that he knows to ask our human resources office for your application materials. It is helpful to send copies to Joe Wells of any electronic files you submit. * Anyone who might need a work permit if hired (usually someone who is not a citizen of an EEA country) should also do the following. In addition to possibly being e-mailed or faxed, each recommendation letter should also be sent by post on official-looking headed stationery paper and should include details on your whereabouts over the last two years. A work permit application also needs copies of any degree certificates, so it is a good idea to send those also at the same time as you send the rest of your application. Work permit applications can take quite some time for the UK's Home Office to process, so please avoid delays. For your information, it is helpful if the writers of reference letters provide details of: * the capacity in which they know the candidate, * the candidate's skills, abilities and performance in relation to the post applied for, * the candidate's employment record including details of the candidate's role and service dates, * their view of the candidate's suitability for the post as a whole, in light of the attached details and their knowledge of the candidate's experience and abilities, * any further relevant information which would assist us in making an appointment. From icfp.publicity at googlemail.com Wed Jan 17 17:03:31 2007 From: icfp.publicity at googlemail.com (Matthew Fluet (ICFP Publicity Chair)) Date: Wed, 17 Jan 2007 16:03:31 -0600 Subject: [TYPES/announce] ICFP07 Call for Papers Message-ID: <53ff55480701171403i3250b7c0lf6eebc403ab3b66e@mail.gmail.com> Call for Papers ICFP 2007: International Conference on Functional Programming Freiburg, Germany, 1-3 October 2007 ICFP 2007 seeks original papers on the art and science of functional programming. Submissions are invited on all topics from principles to practice, from foundations to features, from abstraction to application. The scope includes all languages that encourage functional programming, including both purely applicative and imperative languages, as well as languages with objects and concurrency. Particular topics of interest include * Applications and domain-specific languages: systems programming; scientific and numerical computing; symbolic computing; artificial intelligence; databases; graphical user interfaces; multimedia programming; scripting; system administration; distributed-systems and web programming; XML processing; security * Foundations: formal semantics; lambda calculus; type theory; monads; continuations; control; state; effects * Design: algorithms and data structures; modules; type systems; concurrency and distribution; components and composition; relations to object-oriented or logic programming * Implementation: abstract machines; compile-time and run-time optimization; just-in-time compilers; memory management; parallel hardware; interfaces to foreign functions, services, components or low-level machine resources * Transformation and analysis: abstract interpretation; partial evaluation; program transformation * Software-development techniques: design patterns; specification; verification; validation; debugging; test generation; tracing; profiling * Practice and experience: novel results drawn from experience in education or industry * Functional pearls: elegant, instructive examples of functional programming A functional pearl need not report original research results, but it must be instructive, elegant, and fun. ICFP 2007 also seeks Experience Reports. An Experience Report is a short paper (2-4 pages) which need not present novel results, but which should provide evidence that functional programming really works or should describe obstacles that prevented it from working. Detailed guidelines appear below. What's new this year? ~~~~~~~~~~~~~~~~~~~~~ Experienced ICFP authors may want to pay special attention to the points below, which are new this year. * Double-blind review * Author-date citations * Supplemental material in a separate document, not appended to the main text * Morning deadline (but equivalent to late afternoon or early evening in many time zones of interest) * Experience Reports Instructions for authors ~~~~~~~~~~~~~~~~~~~~~~~~ By 11:00 AM Friday, 6 April 2007, Samoan time, submit an abstract of at most 300 words and a full paper of at most 12 pages or an Experience Report of at most 4 pages. Submissions will be accepted electronically, at a URL to be named later. The deadline is set at Samoan time, so if your submission is in by 11:00 AM Friday according to your local time, wherever you are, the submission will be on time. The world clock at http://www.timeanddate.com/worldclock/fixedtime.html?month=4&day=6&year=2007&hour=11&min=0&sec=0&p1=282 can give you the equivalent in your local time, e.g., 3:00 PM Friday in Portland, 6:00 PM Friday in Boston, and midnight Friday in Freiburg. The deadline is firm. Your submission should explain its contributions in both general and technical terms, clearly identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. Make the technical content understandable to a broad audience. Each submission must adhere to SIGPLAN's republication policy, which appears in full at http://www.acm.org/sigplan/republicationpolicy.htm. The policy means in part that your paper may not have already appeared in a journal, conference, or workshop with published proceedings; that you may not submit substantially the same work simultaneously to ICFP and to another venue; and that your submission must discuss any closely related material, including your own, that was previously accepted at a journal, conference, or workshop with or without published proceedings. Full details of the policy are available at the SIGPLAN site. If you are in any doubt about whether this policy applies to your paper, either consult the program chair in advance or notify the chair when you submit. To do otherwise risks summary rejection of your submission. If your submission is accepted, you must assign copyright to ACM. Proceedings will be published by the ACM Press. Double-blind review ~~~~~~~~~~~~~~~~~~~ To increase confidence in the fairness and objectivity of the reviewing process, reviewing will be double blind. Make it possible for reviewers to evaluate your paper without having to know who you are. It should suffice to omit your names from your submission and to avoid revealing your identity through citation; detailed guidelines are available at http://icfp07.eecs.harvard.edu/blind.html. Formatting ~~~~~~~~~~ Your submission must be printable on US Letter sized paper and be either PDF or PostScript that is interpretable by Ghostscript. If this requirement is a hardship, make contact with the program chair at least one week before the deadline. Your submission must be at most 12 pages (4 pages for an Experience Report), including bibliography and figures, in the standard ACM conference format: two columns, nine-point font on a ten-point baseline, with pages 20pc (3.33in) wide and 54pc (9in) tall, with a column gutter of 2pc (0.33in). (A suitable LaTeX class file is available from SIGPLAN; see http://www.acm.org/sigs/sigplan/authorInformation.htm. Categories, keywords, and so on are optional.) If you wish to supply material beyond the 12-page limit, up to and including a full technical report, you may attach a separate document to your submission, on the understanding that reviewers are not expected to read it. (As a particular example, if you feel that your submission should be supported by a lengthy technical report, do not cite such a technical report on the web, since doing so would reveal your identity. Please instead attach that report to your submission.) Detailed instructions for attaching supplementary documents will be available on the submission web site. The length limit is firm; submissions that do not meet these guidelines will not be considered. Citation ~~~~~~~~ We recommend (but do not require) that you put your citations into author-date form. This procedure makes your paper easier to review. For example, if you cite a result on testing as ``(Claessen and Hughes 2000)'', many reviewers will recognize the result instantly. On the other hand, if you cite it as ``[4]'', even the best-informed reviewer has to page through your paper to find the reference. By using author-date form, you enable a knowledgeable reviewer to focus on content, not arbitrary numbering of references. LaTeX users can simply use the natbib package along with the plainnat bibliography style. Author response ~~~~~~~~~~~~~~~ You will have a 48-hour period (11:00 23 May to 11:00 25 May 2007 Samoa time) to read and respond to reviews. Details of the author-response process will be available as it approaches. Special categories of papers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In addition to research papers, ICFP solicits two kinds of papers that do not require original research contributions: functional pearls, which are full papers, and Experience Reports, which are limited to four pages. Authors submitting such papers may wish to consider the following advice. Functional pearls ~~~~~~~~~~~~~~~~~ To paraphrase both Jon Bentley and Richard Bird, the ideal pearl goes beyond solid engineering into the realm of insight and creativity. Just as a natural pearl grows from a grain of sand that has irritated an oyster, a topnotch functional pearl should grow from a real problem that has irritated a programmer. A pearl should be polished, elegant, instructive, and entertaining. Ideally it should teach important programming techniques and fundamental design principles. Past pearls have included instructive examples of program calculation or proof, nifty presentations of old or new data structures, and interesting applications and programming techniques. Papers submitted to ICFP as pearls often miss the mark, by being too trivial, too complicated, or somehow not quite the elegant solution one hopes for. The key to an accepted pearl is polishing. Your pearl is likely to be rejected if your readers get bored, if the material gets too complicated, if too much specialized knowledge is needed, or if the writing is distasteful. Richard Bird advises: * Throw away the rule book for writing research papers. * Get in quick; get out quick. * Be self-contained; don't go deep into related work, with lengthy references. * You are telling a story, so some element of surprise is welcome. * Above all, be engaging. * Give a talk on the pearl to non-specialists, your students, or your department. If you changed the order of presentation for the talk, consider using the new order in the next draft. * Put the pearl away for a while, then take it out and polish it again. Experience reports ~~~~~~~~~~~~~~~~~~ ICFP has long solicited submissions on the practice and experience of functional programming. But reports of experience are inherently different from research papers, and when judged by the criteria of scientific merit, novelty, or research contribution, they have not competed well against traditional ICFP submissions. Yet we believe that the functional- programming community would benefit from being able to draw on and cite the experience of others. For this reason, we have introduced the ICFP Experience Report. Unlike a normal ICFP paper, the purpose of an Experience Report is not to add to the body of knowledge of the functional-programming community. Rather, the purpose of an Experience Report is to help create a body of published, refereed, citable *evidence* that functional programming really works---or to describe obstacles that prevented it from working. An Experience Report is distinguished from a normal ICFP paper by its title, by its length, and by the criteria used to evaluate it. * Both in the proceedings and in any citations, the title of each accepted Experience Report must begin with the words "Experience Report", followed by a colon. * Experience Reports are limited in length: the suggested length is 2 pages and the maximum length is 4 pages. Each accepted Experience Report will be presented at the conference, but depending on the number of Experience Reports and regular papers accepted, authors of Experience Reports may be asked to give shorter talks. * Because the purpose of Experience Reports is to enable our community to accumulate a published, citable body of evidence about the efficacy of functional programming, an acceptable Experience Report need not present novel results or conclusions. It is sufficient if the Report states a clear thesis and provides supporting evidence. The thesis must be relevant to ICFP, but it need not be novel. The program committee will accept or reject Experience Reports based on whether they judge the evidence to be convincing. Anecdotal evidence will be acceptable provided it is well argued and the author explains what efforts were made to gather as much evidence as possible. The committee will be especially convinced by evidence that includes *comparisons* of situations before and after the introduction or discontinuation of functional programming. Evidence drawn from a single person's experience may be sufficient, but more weight will be given to evidence drawn from the experience of groups of people. Possible topics for an Experience Report include, but are not limited to * Insights gained from real-world projects using functional programming * Comparison of functional programming with conventional programming in the context of an industrial project or a university curriculum * Project-management, business, or legal issues encountered when using functional programming in a real-world project * Curricular issues encountered when using functional programming in education * Real-world constraints that created special challenges for an implementation of a functional language or for functional programming in general An Experience Report should be short and to the point: if functional programming worked for you in the same ways it has worked for others, you need only to summarize the results---the main part of your paper should discuss how well it worked and in what context. Most readers will not want to know all the details of your project and its implementation, but please characterize your project and its context well enough so that readers can judge to what degree your experience is relevant to their own projects. Be especially careful to highlight any unusual aspects of your project. Also keep in mind that specifics about your project are more valuable than generalities about functional programming; for example, it is more valuable to say that your team delivered its software a month ahead of schedule than it is to say that functional programming made your team more productive. If your paper not only describes experience but also presents new technical results, or if your experience refutes cherished beliefs of the functional-programming community, you may be better off submitting it as a full paper, which will be judged by the usual criteria of novelty, originality, and relevance. If you unsure in which category to submit, the program chair will be happy to help you decide. Other information ~~~~~~~~~~~~~~~~~ Conference Chair ~~~~~~~~~~~~~~~~ Ralf Hinze (Universit?t Bonn) Program Chair ~~~~~~~~~~~~~ Norman Ramsey Harvard University Cambridge, MA, 02148 USA Email: icfp07 at eecs.harvard.edu Phone: +1 617 496 8615 Mail sent to the address above is filtered for spam. If you send mail and do not receive a prompt response, particularly if the deadline is looming, feel free to telephone and reverse the charges. Program Committee ~~~~~~~~~~~~~~~~~ Nick Benton (Microsoft Research) Matthew Fluet (Toyota Technological Institute) Jeremy Gibbons (University of Oxford) Kevin Hammond (University of St Andrews) Bastiaan Heeren (Utrecht University) Graham Hutton (University of Nottingham) Mark P. Jones (Portland State University) Gabriele Keller (University of New South Wales) Fabrice Le Fessant (INRIA/LIX, France) Todd Millstein (UCLA) Mike Sperber (DeinProgramm) Christopher A. Stone (Harvey Mudd College) Andrew Tolmach (Portland State University and INRIA Rocquencourt) Janis Voigtl?nder (Technische Universit?t Dresden) Stephanie Weirich (University of Pennsylvania) Important Dates ~~~~~~~~~~~~~~~ Submission: 11:00 6 April 2007, Samoa time (AST) Author response: 11:00 23 May to 11:00 25 May 2007 (AST) Notification: 8 June 2007 Final papers due: 20 July 2007 ICFP 2007 Web Site ~~~~~~~~~~~~~~~~~~ http://www.informatik.uni-bonn.de/~ralf/icfp07.html Special Issue of JFP ~~~~~~~~~~~~~~~~~~~~ Authors of the best final papers, as determined by the program committee, will be invited to submit journal versions for a special issue of the Journal of Functional Programming. From phil at site.uottawa.ca Thu Jan 18 09:36:21 2007 From: phil at site.uottawa.ca (Phil Scott) Date: Thu, 18 Jan 2007 09:36:21 -0500 (EST) Subject: [TYPES/announce] Fields Workshop on Traced Monoidal Cats (Second Announcement) Message-ID: Dear Colleagues: We would like to announce the following: ============================================================== A Fields Institute Sponsored Workshop Recent advances in category theory and logic: Applications of traces to algebra, analysis and categorical logic University of Ottawa April 28-30, 2007 URL: http://aix1.uottawa.ca/~scpsg/Fields07/Fields07.traces.html +++++++++++++++++++++++++++++++++++++++++++++++ The abstract theory of traces has had a fundamental impact on a variety of fields within mathematics. These range from functional analysis and noncommutative geometry to topology and knot theory, and more recently to logic and theoretical computer science. The theory of traced monoidal categories, due to Joyal, Street and Verity, is an attempt to unify various notions of trace that occur in these diverse branches of mathematics. More recent developments include several theories of partial traces in monoidal categories. The Logic and Foundations of Computing Group at the University of Ottawa, with funding from the Fields Institute, is proud to host a workshop to explore these topics. The purpose of this workshop is to bring together researchers in these fields to look for common developments, models, and applications of trace theory. Among the applications are various notions of parametrized traces arising in operator algebras, in the theory of feedback and recursion in theoretical computer science, in braid closure in knot theory, and in dynamics of proofs as expressed by Linear Logic and the Geometry of Interaction. Some invited speakers include: Samson Abramsky (Oxford) Robin Cockett (Calgary) Andre Joyal (UQAM) Louis Kauffman (Illinois) Mathias Neufang (Carleton) Timothy Porter (Bangor) We will be announcing further speakers shortly. This is intended to be a workshop, with student participation in mind, including introductory lectures. We will have some funding for student travel and accommodation. Students interested in receiving financial aid should contact the organizers by January 30th. Anyone interested in attending or contributing a talk should contact us by the above date. We hope to see you there. The organizers: Phil Scott (phil at site.uottawa.ca) Rick Blute (rblute at uottawa.ca) Pieter Hofstra (hofstrap at cpsc.ucalgary.ca) From morazanm at shu.edu Sat Jan 20 08:34:48 2007 From: morazanm at shu.edu (Marco T Morazan) Date: Sat, 20 Jan 2007 08:34:48 -0500 Subject: [TYPES/announce] Final Call for Papers: TFP 2007, New York, USA Message-ID: CALL FOR PAPERS Trends in Functional Programming 2007 New York, USA April 2-4, 2007 http://cs.shu.edu/tfp2007/ NEW: Abstract submission is now opened! Link: http://cs.shu.edu/tfp2007/submissions.html NEW: Invited Talk: John McCarthy, Standford University The symposium on Trends in Functional Programming (TFP) is an international forum for researchers with interests in all aspects of functional programming languages, focusing on providing a broad view of current and future trends in Functional Programming. It aspires to be a lively environment for presenting the latest research results through acceptance by extended abstracts. A formal post-symposium refereeing process then selects the best articles presented at the symposium for publication in a high-profile volume. TFP 2007 is co-hosted by Seton Hall University and The City College of New York (CCNY) and will be held in New York, USA, April 2-4, 2007 at the CCNY campus. SCOPE OF THE SYMPOSIUM The symposium recognizes that new trends may arise through various routes. As part of the Symposium's focus on trends we therefore identify the following five article categories. High-quality articles are solicited in any of these categories: Research Articles leading-edge, previously unpublished research work Position Articles on what new trends should or should not be Project Articles descriptions of recently started new projects Evaluation Articles what lessons can be drawn from a finished project Overview Articles summarizing work with respect to a trendy subject Articles must be original and not submitted for simultaneous publication to any other forum. They may consider any aspect of functional programming: theoretical, implementation-oriented, or more experience-oriented. Applications of functional programming techniques to other languages are also within the scope of the symposium. Articles on the following subject areas are particularly welcomed: o Dependently Typed Functional Programming o Validation and Verification of Functional Programs o Debugging for Functional Languages o Functional Programming and Security o Functional Programming and Mobility o Functional Programming to Animate/Prototype/Implement Systems from Formal or Semi-Formal Specifications o Functional Languages for Telecommunications Applications o Functional Languages for Embedded Systems o Functional Programming Applied to Global Computing o Functional GRIDs o Functional Programming Ideas in Imperative or Object-Oriented Settings (and the converse) o Interoperability with Imperative Programming Languages o Novel Memory Management Techniques o Parallel/Concurrent Functional Languages o Program Transformation Techniques o Empirical Performance Studies o Abstract/Virtual Machines and Compilers for Functional Languages o New Implementation Strategies o any new emerging trend in the functional programming area If you are in doubt on whether your article is within the scope of TFP, please contact the TFP 2007 program chair, Marco T. Morazan, at tfp2007 at shu.edu. SUBMISSION AND DRAFT PROCEEDINGS Acceptance of articles for presentation at the symposium is based on the review of extended abstracts (6 to 10 pages in length) by the program committee. Accepted abstracts are to be completed to full papers before the symposium for publication in the draft proceedings and on-line. Further details can be found at the TFP 2007 website. POST-SYMPOSIUM REFEREEING AND PUBLICATION In addition to the draft symposium proceedings, we intend to continue the TFP tradition of publishing a high-quality subset of contributions in the Intellect series on Trends in Functional Programming. IMPORTANT DATES Abstract Submission: February 1, 2007 Notification of Acceptance: February 20, 2007 Registration Deadline: March 2, 2007 Camera Ready Full Paper Due: March 9, 2007 TFP Symposium: April 2-4, 2007 PROGRAMME COMMITTEE John Clements California Polytechnic State University, USA Marko van Eekelen Radboud Universiteit Nijmegen, The Netherlands Benjamin Goldberg New York University, USA Kevin Hammond University of St. Andrews, UK Patricia Johann Rutgers University, USA Hans-Wolfgang Loidl Ludwig-Maximilians Universit?t M?nchen, Germany Rita Loogen Philipps-Universit?t Marburg, Germany Greg Michaelson Heriot-Watt University, UK Marco T. Moraz?n (Chair) Seton Hall University, USA Henrik Nilsson University of Nottingham, UK Chris Okasaki United States Military Academy at West Point, USA Rex Page University of Oklahoma, USA Ricardo Pena Universidad Complutense de Madrid, Spain Benjamin C. Pierce University of Pennsylvania, USA John Reppy University of Chicago, USA Ulrik P. Schultz University of Southern Denmark, Denmark Clara Segura Universidad Complutense de Madrid, Spain Jocelyn S?rot Universit? Blaise Pascal, France Zhong Shao Yale University, USA Olin Shivers Georgia Institute of Technology, USA Phil Trinder Heriot-Watt University, UK David Walker Princeton University, USA ORGANIZATION Symposium Chair: Henrik Nilsson, University of Nottingham, UK Programme Chair: Marco T. Morazan, Seton Hall University, USA Treasurer: Greg Michaelson, Heriot-Watt University, UK Local Arrangements: Marco T. Morazan, Seton Hall University, USA ********************************************************************************** Prof. Marco T. Morazan Dept. of Mathematics and Computer Science Seton Hall University "On theories such as these we cannot rely. Proof we need. Proof!" -- Yoda, Jedi Master -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20070120/fc5ce121/attachment.htm From Jeremy.Gibbons at comlab.ox.ac.uk Mon Jan 22 09:45:48 2007 From: Jeremy.Gibbons at comlab.ox.ac.uk (Jeremy Gibbons) Date: Mon, 22 Jan 2007 14:45:48 GMT Subject: [TYPES/announce] Call for participation and abstracts: BCTCS, Oxford, 2-5 Apr Message-ID: <200701221445.l0MEjmV7016612@softeng.comlab.ox.ac.uk> (apologies for any duplicate cross-postings you may receive) +--------------------------------------------------------------------+ 23rd British Colloquium for Theoretical Computer Science BCTCS 2007 2-5 April 2007 St Anne's College, Oxford http://cms.brookes.ac.uk/bctcs2007/ The purpose of BCTCS is to provide a forum in which researchers in theoretical computer science can meet, present research findings, and discuss developments in the field. It also aims to provide an environment in which PhD students can gain experience in presenting their work, and benefit from contact with established researchers. SCOPE All aspects of theoretical computer science, including automata theory, algorithms, complexity theory, semantics, formal methods, concurrency, types, languages and logics. Computer scientists and mathematicians are welcome to attend, as are participants from outside the UK. PROGRAMME The programme will consist of nearly 3 days worth of invited and contributed talks, beginning at 5.30pm on Monday 2nd April and concluding at 1pm on Thursday 5th April 2007. The abstracts of the talks will be published in the Bulletin of the European Association for Theoretical Computer Science (EATCS). The invited speakers are as follows: Dimitris Achlioptas, University of California, Santa Cruz, U.S.A. "Random Constraint Satisfaction Problems: from Physics to Algorithms" Steven Alpern, The London School of Economics and Political Science "Search Games and Utilitarian Postman Paths on Networks" Julian Bradfield, University of Edinburgh (BCS-FACS Lecturer in Formal Methods) Georg Gottlob, University of Oxford "Living with Computational Complexity" (This is Prof. Gottlob's inaugural lecture at Oxford University.) Bob Harper, Carnegie Mellon University, U.S.A. Richard Jozsa, University of Bristol Kristina Vuskovic, University of Leeds (LMS Lecturer in Discrete Mathematics) LOCATION The 2007 colloquium will be held at St Anne's College, Oxford, one of the colleges of the University of Oxford, and hosted by the computing departments of both Oxford Brookes and Oxford universities, Oxford itself is known as the "City of Dreaming Spires", and has been home to both royalty and scholars for over 800 years. REGISTRATION Registration for BCTCS2007 is open, via the web page. The deadline for registration and submission of abstracts for proposed talks is 16th February 2007. The registration fee is 340 UK pounds, including accommodation and meals, and the day rate is 145 UK pounds. A number of free registrations for UK-based PhD students are available. SPONSORS The colloquium is sponsored by EPSRC, BCS-FACS, and also the London Mathematical Society. FURTHER DETAILS Google search - BCTCS 2007 Web page - http://cms.brookes.ac.uk/bctcs2007/ +--------------------------------------------------------------------+ From afelty at site.uottawa.ca Tue Jan 23 11:50:20 2007 From: afelty at site.uottawa.ca (Amy Felty) Date: Tue, 23 Jan 2007 11:50:20 -0500 (EST) Subject: [TYPES/announce] CADE 2007 2nd Call for Papers Message-ID: UPDATE: invited speakers, affiliated workshops, travel grants, submissions open Deadline for abstract submission: February 16! 2nd Call for Papers CADE-21 21st International Conference on Automated Deduction International University Bremen, Germany July 17-20, 2007 (workshops July 15-16) http://www.cadeconference.org/meetings/cade21 CALL FOR PAPERS CADE is the major forum for the presentation of research in all aspects of automated deduction. - Logics of interest include propositional, first-order, equational, higher-order, classical, intuitionistic, constructive, modal, temporal, many-valued, substructural, description, and meta-logics, logical frameworks, type theory and set theory. - Methods of interest include resolution, tableaux, term rewriting, induction, unification, constraint solving, SAT solving, decision procedures, saturation, model generation, model checking, natural deduction, sequent calculi, proof planning, proof presentation, proof checking, and explanation. - Applications of interest include hardware and software development, systems analysis and verification, deductive databases, functional and logic programming, computer mathematics, natural language processing, computational linguistics, robotics, planning, knowledge representation, and other areas of AI. Invited speakers: Peter Baumgartner, NICTA and Australian National University Rustan Leino, Microsoft Research Colin Stirling, University of Edinburgh Ashish Tiwari, SRI International Affiliated workshops (July 15-16, 2007): ADDCT - Automated Deduction: Decidability, Complexity, Tractability CVF - Fourth International Workshop on Constraints in Formal Verification DISPROVING - Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability ESARLT - Empirically Successful Automated Reasoning in Large Theories ISABELLE-WS - Isabelle Workshop LFMTP - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice VERIFY - 4th International Verification Workshop Woody Bledsoe student travel awards: Nominations must be made by June 1; details available at http://www.cadeconference.org/meetings/cade21/travelawards.html Paper submission: Submission is electronic in PostScript or PDF format via the EasyChair system. Submitted papers must conform to the Springer LNCS style, preferrably using LaTeX2e and the Springer llncs class files available at http://www.springer.com/lncs. Submissions can be full papers, for work on foundations, applications, or implementation techniques (15 pages), as well as system descriptions (5 pages), for describing publicly available systems. The proceedings will be published in the Springer LNCS series. Submissions are now open at http://www.easychair.org/CADE21/ Important dates: Submission of title and abstract: February 16, 2007 Submission papers: February 23, 2007 Notification of acceptance: April 16, 2007 Final version due: May 11, 2007 Workshops and tutorials: July 15-16, 2007 Conference: July 17-20, 2007 Conference Chair: Michael Kohlhase (IUB) Workshop and Tutorial Chair: Christoph Benzmueller (Cambridge) Program Chair: Frank Pfenning (CMU) From Giuseppe.Castagna at ens.fr Tue Jan 23 17:51:59 2007 From: Giuseppe.Castagna at ens.fr (Giuseppe Castagna) Date: Tue, 23 Jan 2007 23:51:59 +0100 Subject: [TYPES/announce] Position available at University Paris 7 Message-ID: <45B6918F.3080405@ens.fr> The laboratory PPS of University Paris 7 is looking for candidates for a one year position, available immediately, around the CDuce project. CDuce is a strongly typed functional programming language for XML (see http://www.cduce.org) whose design and run-time are directly based on its type systems. Its compiler is implemented in OCaml. According to the profile of the recruited person the position will focus more on the development environment (e.g.: libraries for web development or web services, Eclipse plugins, Windows port) or on the research aspects (e.g.: concurrency, typing, subtyping, distribution, verification) around CDuce. Candidates should be fluent in OCaml or in another functional language. Experience in Web development, environments for software development and/or XML would be useful as well. The annual gross salary will be around 28.000 Euros. If interested please send a mail to staff at cduce.org as soon as possible. Giuseppe Castagna From laurie at tratt.net Wed Jan 24 09:24:30 2007 From: laurie at tratt.net (Laurence Tratt) Date: Wed, 24 Jan 2007 14:24:30 +0000 Subject: [TYPES/announce] MODELS 2007 Call for Contributions Message-ID: <20070124142453.GA1629@phase.home.tratt.net> =========================================================================== MODELS 2007 -- First Call for Contributions ACM/IEEE 10th International Conference on Model-Driven Engineering Languages and Systems September 30 - October 5, 2007 Nashville (TN), USA http://www.modelsconference.org/ =========================================================================== The past decade has witnessed an explosion of interest in advanced techniques for expressing design intent at a higher level of abstraction than third-generation programming languages and keeping abstract models of complex software systems in sync with the underlying code. MODELS 2007 (formerly the UML series of conferences) is the premier conference in model-driven approaches to software development. Scientific papers: We invite scientific research papers describing innovative research on model-driven engineering and other aspects of modeling in the development process. Experience papers: We invite experience papers that focus on reporting project experience with model-driven engineering. Please visit the conference website http://www.modelsconference.org/ for more information. IMPORTANT DATES Experience and Scientific Papers deadlines: Abstracts: March 19, 2007 Submissions: April 2, 2007 Workshop Proposals deadline: April 2, 2007 Tutorial Proposals deadline: May 1, 2007 Doctoral and Educators Symposiums, Vendor Tools Exhibits, Academic Posters and Demos, and Panels deadline: May 1, 2007 Submission guidelines are available from the website. Authors of best papers from the conference will be invited to revise and submit extended versions of their papers for publication consideration in a special issue of Software and Systems Modeling (Springer). Proposals for advanced workshops, tutorials and posters are requested. From Jeremy.Gibbons at comlab.ox.ac.uk Thu Jan 25 02:40:18 2007 From: Jeremy.Gibbons at comlab.ox.ac.uk (Jeremy.Gibbons@comlab.ox.ac.uk) Date: Thu, 25 Jan 2007 07:40:18 GMT Subject: [TYPES/announce] IFM2007 Final call for contributions Message-ID: <200701250740.l0P7eIbZ023479@mercury.comlab.ox.ac.uk> ---------------------------------------------------------------------- IFM 2007 Sixth International Conference on Integrated Formal Methods 2nd - 6th July 2007, Oxford, UK http://www.ifm2007.org Final Call for Contributions Contributions to the technical programme of IFM 2007, including papers for the special session on Unifying Theories of Programming, and proposals for workshops and tutorials, are invited. The deadline for submission has been extended to 5th February 2007. See the calls at http://www.ifm2007.org Papers should not exceed 20 pages in length, and should be prepared in accordance with the publisher's guidelines; style files and templates are available at http://www.ifm2007.org/LNCS.html Both .doc and .pdf formats are acceptable. Electronic submission is possible via the conference website. Authors will be notified on or before March 15th. ---------------------------------------------------------------------- From phil at site.uottawa.ca Thu Jan 25 13:35:28 2007 From: phil at site.uottawa.ca (Phil Scott) Date: Thu, 25 Jan 2007 13:35:28 -0500 (EST) Subject: [TYPES/announce] Postdoctoral position at U. Ottawa Message-ID: Research Fellow/Postdoc position in Category Theory, Logic and Computation, University of Ottawa The Logic Group in the Department of Mathematics and Statistics at the University of Ottawa is looking to hire at least one research fellow/postdoc beginning in September, 2007. The positions are in any area of category theory, categorical logic, and related areas of theoretical computer science. Research fellows/postdocs will participate in the activities of the Logic and Foundations of Computation Group. This group includes faculty and students from several different Ottawa-area universities. In the Math Department, the Logic Group currently includes 4 faculty members (R. Blute, P. Hofstra, P.E. Parent and P. Scott), as well as a number of postdocs and graduate students. For more information about our team, see http://www.site.uottawa.ca/~phil/lfc/. The research fellowships/postdocs are initially for one year, with a possible renewal for a second year. Duties include research and the teaching of two one-semester mathematics courses. Potential applicants should contact one of us (preferably cc to all):: Richard Blute (rblute at uottawa.ca) Pieter Hofstra (phofstra at uottawa.ca) Paul-Eugene Parent (pparent at uottawa.ca) Philip Scott (phil at site.uottawa.ca) immediately by email to indicate their interest. They should then also send a curriculum vitae, a research plan, and arrange for three confidential letters of recommendation, with one addressing teaching, to be sent to Professor Victor Leblanc, Chairman, Department of Mathematics and Statistics, University of Ottawa, Ottawa, ON Canada, K1N 6N5. Applicants are also encouraged to include up to three copies of their most significant publications. Those who have already applied for a position will of course be considered and do not have to re-send an application, although it would be wise to send one of us an email. From Belaid.Benhamou at cmi.univ-mrs.fr Fri Jan 26 11:46:57 2007 From: Belaid.Benhamou at cmi.univ-mrs.fr (benhamou) Date: Fri, 26 Jan 2007 17:46:57 +0100 Subject: [TYPES/announce] Last CFP of TABLEAUX 2007 In-Reply-To: <458C0FEC.4030407@cmi.univ-mrs.fr> References: <200601291711.k0THB45e018819@birkhoff.cas.mcmaster.ca> <458C0FEC.4030407@cmi.univ-mrs.fr> Message-ID: <45BA3081.6040905@cmi.univ-mrs.fr> (We apologize for multiple copies of this Call) ======================================================================== %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Call for Papers, Call for Tutorials and %% %% Call for Workshop Proposals %% %% %% %% 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/ IMPORTANT DATES Tutorial proposal submission deadline: January 10, 2007 (Now closed) Notification of acceptance of tutorials: January 20, 2007 Workshop proposal submission deadline: January 31, 2007 Notification of acceptance of workshops: February 15, 2007 Title and abstract submission deadline: February 2, 2007 Paper submission deadline: February 9, 2007 Notification of acceptance of papers: April 2, 2007 Final version of papers due: April 16, 2007 Conference: July 3-6, 2007 GENERAL INFORMATION This conference is the 16th in a series of international meetings on Automated Reasoning with Analytic Tableaux and Related Methods. In July 2007, the conference will be held in Aix en Provence, France. The conference proceedings will be published in LNAI series as in the previous editions of the conference. See http://tableaux2007.univ-cezanne.fr/ for more information on TABLEAUX 2007, and http://i12www.ira.uka.de/TABLEAUX for information about the TABLEAUX conference series. 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. Topics of interest include (but are not restricted to): * analytic tableaux for various logics (theory and applications) * related techniques and concepts, e.g., model checking and BDDs * related methods (model elimination, sequent calculi, connection method, ...) * new calculi and methods for theorem proving in classical and non-classical logics (modal, description, intuitionistic, linear, temporal, many-valued...) * systems, tools, implementations and applications. TABLEAUX 2007 puts a special emphasis on applications. Papers describing applications of tableaux and related methods in areas such as, for example, hardware and software verification, knowledge engineering, semantic web, etc. are particularly invited. One or more tutorials and workshops will be part of the conference program. SUBMISSIONS The conference will include contributed papers, tutorials, system descriptions, position papers and invited lectures. Submissions are invited in four categories: A Research papers (reporting original theoretical and/or experimental research, up to 15 pages) B System descriptions (up to 5 pages) C Position papers and brief reports on work in progress D Tutorials in all areas of analytic tableaux and related methods from academic research to applications (proposals up to 5 pages) Submissions in categories A and B will be reviewed by peers, typically members of the program committee. They must be unpublished and not submitted for publication elsewhere. Accepted papers in these categories will be published in the conference proceedings . For category B submissions a working implementation must exist and be available to the referees. Submissions in category C will be reviewed by members of the program committee and a collection of the accepted papers in this category will be published as a Technical Report of the LSIS/Universit? Paul C?zanne. Tutorial submissions (Category D) may be at introductory, intermediate, or advanced levels. Novel topics and topics of broad interest are preferred. The submission should include the title, the author, the topic of the tutorial, its level, its relevance to conference topics, and a description of the interest and the scientific contents of the proposed tutorial. Tutorial proposals will be reviewed by members of the program committee. Authors of accepted papers are expected to present their work at the conference. CALL FOR WORKSHOP PROPOSALS TABLEAUX 2007 launches a Call for Workshop Proposal on specialised subjects in the range of the conference topics. We can accept up to 2 proposals. The proposals are reviewed by members of the PC committee. The purpose of a workshop is to offer an opportunity of presenting novel ideas, ongoing research, and to discuss the state of the art of an area in a less formal but more focused way than the conference itself. It is also a good opportunity for young researchers to present their own work and to obtain feedback. The format of a workshop is left to the organizers, but it is expected to contain significant time for discussion. The intended schedule is for one-day workshops. Further information and instructions about submissions will be available on the conference website at http://tableaux2007.univ-cezanne.fr/. PROGRAM COMMITTEE Nicola Olivetti, LSIS, Paul C?zanne University, Marseilles, France (Chair) Peter Baumgartner, Peter Baumgartner, NICTA, Canberra, Australia Bernhard Beckert, University of Koblenz-Landau, Germany Patrick Blackburn, INRIA Lorraine, France Marta Cialdea, University of Roma 3, Italy Roy Dyckhoff, University of St Andrews, Scotland Christian G. Ferm?ller, University of Wien, Austria Ulrich Furbach, University of Koblenz-Landau, Germany Didier Galmiche, LORIA, Henri Poincar? University, Nancy, France Martin Giese, RICAM, Austrian Academy of Sciences, Linz, Austria Rajeev P. Gor?, Australian National University, Canberra, Australia Jean Goubault-Larrecq, LSV, ENS Cachan, France Reiner H?hnle, University of Chalmers, Gothenburg, Sweden Ullrich Hustadt, University of Liverpool, UK Christoph Kreitz, University of Potsdam, Germany Carsten Lutz, University of Dresden, Germany Angelo Montanari, University of Udine, Italy Ugo Moscato, University of Milano-Bicocca, Italy Neil V. Murray, ILS Institute, University at Albany, USA Ilkka Niemel?, Helsinki University of Technology, Finland Lawrence C. Paulson, University of Cambridge, UK Camilla Schwind, LIF-CNRS, Marseille, France Viorica Sofronie-Stokkermans, Max-Planck-Institut f?r Informatik, Saarbr?cken, Germany (Workshop Chair) Arild Waaler, University of Oslo, Norway ORGANIZING COMMITTEE Conference chair: Nicola Olivetti, LSIS, Paul C?zanne University, Marseilles, France Publicity Chair: Bela?d Benhamou, LSIS, Universit? de Provence, Marseilles, France Local Organisers: Bela?d Benhamou, LSIS, University of Provence, Marseilles, France Djamal Habet, LSIS, Paul C?zanne University, Marseilles, France Philippe J?gou, LSIS, Paul C?zanne University, Marseilles, France Richard Ostrowski, LSIS, University of Provence, Marseilles, France Cyril Pain-Barre, LSIS, University of Mediterranean, Marseilles, France Odile Papini, LSIS, University of Toulon, France Nicolas Prcovic, LSIS, Paul C?zanne University, Marseilles, France Vincent Risch, LSIS, University of Mediterranean, Marseilles, France Pierre Siegel, LSIS, University of Provence, Marseilles, France Cyril Terrioux, LSIS, Paul C?zanne University, Marseilles, France Eric W?rbel, LSIS, University of Toulon, France ===================================================================================== Best regards Bela?d Benhamou (Publicity chair) Universit? de Provence Aix-Marseille I, CMI-LSIS, 39 Joliot-Curie 13453 Mareille cedex 13, France Tel: 0033491113622 Fax: 0033491113692 From nordio at dc.exa.unrc.edu.ar Fri Jan 26 14:08:09 2007 From: nordio at dc.exa.unrc.edu.ar (=?ISO-8859-1?Q?Mart=EDn_Nordio?=) Date: Fri, 26 Jan 2007 16:08:09 -0300 Subject: [TYPES/announce] LASER Summer School on Software Engineering Message-ID: <20070126190748.M34771@dc.exa.unrc.edu.ar> LASER Summer School on Software Engineering Applied Software Verification Practical advances towards a Grand Challenge September 9-15, 2007, Elba, Italy http://laser.inf.ethz.ch Application deadline: April 30, 2007 Goals The LASER school is intended both for researchers (including PhD students) and for professional software engineers and managers who want to benefit from the best in software technology advances. The focus of LASER is resolutely practical, although theory is welcome to establish solid foundations. The format of the school favors extensive interaction between participants and speakers. Topics and speakers The 2007 LASER school is part of the ongoing "Grand Challenge" on software verification, initiated by Tony Hoare. It has a special focus on tools for software verification. This means in particular that it has a highly practical character and will provide participants with a clear view of techologies and tools available today to verify software. The school brings together six speakers, each closely involved with tools for verification: * Thomas Ball, Microsoft Research * G?rard Berry, Esterel Technologies * Tony Hoare, Microsoft Research * Bertrand Meyer, ETH Zurich * Peter M?ller, ETH Zurich * Natarajan Shankar, SRI International How to apply? Use the online registration form available on the LASER website http://laser.inf.ethz.ch. Registration is open until 30 April 2007. The number of participants is strictly limited to ensure quality interaction with the lecturers and the rest of the audience. For more information, visit our website or contact the organizers at laser at se.inf.ethz.ch. Venue As in previous years, LASER is held in the magnificent setting of the Elba island off the coast of Tuscany, easily reachable by plane (Pisa) and train. Time is set aside to avoid the amenities of the 4-star Hotel del Golfo (private beach, tennis court etc.) as well as the natural and cultural riches of Elba, a history-laden jewel of the Mediterranean. -- Departamento de Computaci?n Universidad Nacional de R?o Cuarto From ruy at cin.ufpe.br Sat Jan 27 05:19:38 2007 From: ruy at cin.ufpe.br (ruy@cin.ufpe.br) Date: Sat, 27 Jan 2007 08:19:38 -0200 (BRST) Subject: [TYPES/announce] WoLLIC'2007 - CfP Message-ID: <4965.200.164.147.77.1169893178.squirrel@webmail.cin.ufpe.br> [** sincere apologies for duplicates **] Call for Papers 14th Workshop on Logic, Language, Information and Computation (WoLLIC'2007) Rio de Janeiro, Brazil July 2-5, 2007 WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Each meeting includes invited talks and tutorials as well as contributed papers. The Fourteenth WoLLIC will be held in Rio de Janeiro, Brazil, from July 2 to July 5, 2007, and sponsored by the Association for Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics (IGPL), the European Association for Logic, Language and Information (FoLLI), the European Association for Theoretical Computer Science (EATCS), the Sociedade Brasileira de Computacao (SBC), and the Sociedade Brasileira de Logica (SBL). PAPER SUBMISSION Contributions are invited on all pertinent subjects, with particular interest in cross-disciplinary topics. Typical but not exclusive areas of interest are: foundations of computing and programming; novel computation models and paradigms; broad notions of proof and belief; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection. Proposed contributions should be in English, and consist of a scholarly exposition accessible to the non-specialist, including motivation, background, and comparison with related works. They must not exceed 10 pages (in font 10 or higher), with up to 5 additional pages for references and technical appendices. The paper's main results must not be published or submitted for publication in refereed venues, including journals and other scientific meetings. It is expected that each accepted paper be presented at the meeting by one of its authors. Papers must be submitted electronically at www.cin.ufpe.br/~wollic/wollic2007/instructions.html A title and single-paragraph abstract should be submitted by February 23, and the full paper by March 2 (firm date). Notifications are expected by April 13, and final papers for the proceedings will be due by April 27 (firm date). PROCEEDINGS Proceedings, including both invited and contributed papers, will be published in advance of the meeting. Publication venue: Springer's Lecture Notes in Computer Science. INVITED SPEAKERS: Veronique Cortier (LORIA Nancy) Martin Escardo (Birmingham) Georg Gottlob (Oxford) Achim Jung (Birmingham) Louis Kauffman (U Illinois Chicago) Sam Lomonaco (U Maryland Baltimore) Paulo Oliva (London/QM) John Reif (Duke) Yde Venema (Amsterdam) STUDENT GRANTS ASL sponsorship of WoLLIC'2007 will permit ASL student members to apply for a modest travel grant (deadline: April 1, 2007). See www.aslonline.org/studenttravelawards.html for details. IMPORTANT DATES February 23, 2007: Paper title and abstract deadline March 2, 2007: Full paper deadline (firm) April 12, 2007: Author notification April 26, 2007: Final version deadline (firm) PROGRAM COMMITTEE Samson Abramsky (U Oxford) Michael Benedikt (Bell Labs) Lars Birkedal (ITU Copenhagen) Andreas Blass (U Michigan) Thierry Coquand (Chalmers U, Goteborg) Jan van Eijck (CWI, Amsterdam) Marcelo Finger (U Sao Paulo) Rob Goldblatt (Victoria U, Wellington) Yuri Gurevich (Microsoft Redmond) Hermann Haeusler (PUC Rio) Masami Hagiya (Tokyo U) Joseph Halpern (Cornell U) John Harrison (Intel UK) Wilfrid Hodges (U London/QM) Phokion Kolaitis (IBM Almaden Research Center) Marta Kwiatkowska (U Birmingham) Daniel Leivant (Indiana U) (Chair) Maurizio Lenzerini (U Rome) Jean-Yves Marion (LORIA Nancy) Dale Miller (Polytechnique Paris) John Mitchell (Stanford U) Lawrence Moss (Indiana U) Peter O'Hearn (U London/QM) Prakash Panangaden (McGill, Montreal) Christine Paulin-Mohring (Paris-Sud, Orsay) Alexander Razborov (Steklov, Moscow) Helmut Schwichtenberg (Munich U) Jouko Vaananen (U Helsinki) ORGANISING COMMITTEE Marcelo da Silva Correa (U Fed Fluminense) Renata P. de Freitas (U Fed Fluminense) Ana Teresa Martins (U Fed Ceara') Anjolina de Oliveira (U Fed Pernambuco) Ruy de Queiroz (U Fed Pernambuco, co-chair) Petrucio Viana (U Fed Fluminense, co-chair) WEB PAGE www.cin.ufpe.br/~wollic/wollic2007 --- From miculan at dimi.uniud.it Mon Jan 29 04:44:35 2007 From: miculan at dimi.uniud.it (Marino Miculan) Date: Mon, 29 Jan 2007 10:44:35 +0100 Subject: [TYPES/announce] TYPES 2007 Announce Message-ID: <1B66E747-9C85-4887-BED3-82494E27F53D@dimi.uniud.it> TYPES 2007 Main Conference of the Types Project Cividale, Italy, May 2-5, 2007 http://www.dimi.uniud.it/types07/ This is the latest meeting in a series that started 1992, the last conference was in April 2005 in Nottingham. The topic of the meeting is formal reasoning and computer programming based on Type Theory: languages and computerised tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalisation of mathematics and mathematics education. The conference is organized by the Department of Mathematics and Computer Science of the University of Udine, and takes place in Cividale del Friuli, a medieval town near Udine, Italy. For more information and registration, see: http://www.dimi.uniud.it/types07/ Early registration deadline is *** March 31, 2007 ***. At the registration you will be able to propose your talk and abstract. We will try to accomodate as much as possible the talks which fit into the scope of the TYPES project. There will also be invited lectures. A number of block reservations for the participants of TYPES 2007 have been made at some hotels in Cividale. However, most are only held until *** February 28, 2007 *** (and some until the early registration deadline), so it is highly advisable to make your reservation as soon as possible. See site for details. Please direct all emails related to TYPES 2007 to types07 at dimi.uniud.it The Organisation Comittee Marino Miculan, Ivan Scagnetto, Furio Honsell. From finco07 at cs.brown.edu Mon Jan 29 14:45:30 2007 From: finco07 at cs.brown.edu (FINCO 2007) Date: Mon, 29 Jan 2007 14:45:30 -0500 Subject: [TYPES/announce] final CFP: Foundations of Interactive Computation Message-ID: final call for papers FInCo 2007: FOUNDATIONS OF INTERACTIVE COMPUTATION satellite workshop of ETAPS 2007 Saturday 31 March 2007, Braga, Portugal http://www.cs.brown.edu/sites/finco07 ==================================================== The interaction paradigm provides a new conceptualization of compu- tational phenomena, placing the emphasis on interaction rather than on algorithms; concurrent, distributed, reactive, embedded, component- oriented, agent-oriented and service-oriented systems all exploit interaction as a fundamental paradigm. Contemporary approaches to Software Engineering, Artificial Intelligence, Programming Languages, and Networking are all part of this paradigm change. However, a satis- factory unified foundational framework for interactive computation is still lacking, analogous to the one that Turing Machines and