[Caml-list] PLMMS - last call for papers

LAST CALL FOR PAPERS

Second Workshop on
Programming Languages for Mechanized Mathematics
(PLMMS 2008)

http://events.cs.bham.ac.uk/cicm08/workshops/plmms/

As part of CICM / Calculemus 2008
Birmingham, UK, 28-29 July 2008

This workshop is focused on the intersection of programming languages
(PL) and mechanized mathematics systems (MMS). The latter category
subsumes present-day computer algebra systems (CAS), interactive proof
assistants (PA), and automated theorem provers (ATP), all heading
towards fully integrated mechanized mathematical assistants that are
expected to emerge eventually (cf. the objective of Calculemus).

The two subjects of PL and MMS meet in the following topics, which are
of particular interest to this workshop:

* Dedicated input languages for MMS: covers all aspects of languages
intended for the user to deploy or extend the system, both
algorithmic and declarative ones. Typical examples are tactic
definition languages such as Ltac in Coq, mathematical proof
languages as in Mizar or Isar, or specialized programming
languages built into CA systems. Of particular interest are the
semantics of those languages, especially when current ones are
untyped.

* Mathematical modeling languages used for programming: covers the
relation of logical descriptions vs. algorithmic content. For
instance the logic of ACL2 extends a version of Lisp, that of Coq
is close to Haskell, and some portions of HOL are similar to ML
and Haskell, while Maple tries to do both simultaneously. Such
mathematical languages offer rich specification capabilities,
which are rarely available in regular programming languages. How
can programming benefit from mathematical concepts, without
limiting mathematics to the computational worldview?

* Programming languages with mathematical specifications: covers
advanced "mathematical" concepts in programming languages that
improve the expressive power of functional specifications, type
systems, module systems etc. Programming languages with dependent
types are of particular interest here, as is intentionality vs
extensionality.

* Language elements for program verification: covers specific means
built into a language to facilitate correctness proofs using MMS.
For example, logical annotations within programs may be turned
into verification conditions to be solved in a proof assistant
eventually. How need MMS and PL to be improved to make this work
conveniently and in a mathematically appealing way?

These issues have a very colorful history. Many PL innovations first
appeared in either CA or proof systems first, before migrating into
more mainstream programming languages. Some examples include type
inference, dependent types, generics, term-rewriting, first-class
types, first-class expressions, first-class modules, code extraction
etc. However, such innovations were never aggressively pursued by
builders of MMS, but often reconstructed by programming language
researchers. This workshop is an opportunity to present the latest
innovations in MMS design that may be relevant to future programming
languages, or conversely novel PL principles that improve upon
implementation and deployment of MMS.

We also want to critically examine what has worked, and what has not.
Why are all the languages of mainstream CA systems untyped? Why are the
(strongly typed) proof assistants so much harder to use than a typical
CAS? What forms of polymorphism exist in mathematics? What forms of
dependent types may be used in mathematical modeling? How can MMS
regain the upper hand on issues of "genericity" and "modularity"? What
are the biggest barriers to using a more mainstream language as a host
language for a CAS or PA/ATP?

Invited Talk
------------

Conor McBride (Alta Systems, Northern Ireland) will give an invited
talk "Theorem Proving for the Lazy Programmer"

Submission
----------

Submission works through EasyChair
http://www.easychair.org/conferences/?conf=plmms2008

Two kinds of papers will be considered:

* Full research papers may be up to 12 pages long. Authors of
accepted papers are expected to present their work on the workshop
in a regular talk.

* Position papers may be up to 4 pages long. The workshop
presentation of accepted position papers consists of two parts: a
stimulating statement of certain issues or challenges by the
author, followed by a discussion in the plenum.

Papers should use the usual ENTCS style http://www.entcs.org/prelim.html
(11 point version), and will be reviewed by the program
committee. Informal workshop proceedings will be circulated as a
technical report.

Moreover there will be post-workshop proceedings of improved research
papers, or position papers that have been completed into full papers,
to appear in a special issue of the Journal of Automated Reasoning.
There will be a separate submission and review phase for this, where
papers from both PLMMS 2007 and 2008 will be considered.

Programme Committee
-------------------

Jacques Carette (Co-Chair) (McMaster University, Canada)
John Harrison (Intel Corporation, USA)
Hugo Herbelin (INRIA, Ecole polytechnique, France)
James McKinna (Radboud University Nijmegen, Netherlands)
Ulf Norell (Chalmers University, Sweden)
Bill Page
Christophe Raffalli (Universite de Savoie, France)
Josef Urban (Charles University, Czech Republic)
Stephen Watt (ORCCA, University of Western Ontario, Canada)
Makarius Wenzel (Co-Chair) (Technische Universitaet Muenchen, Germany)
Freek Wiedijk (Radboud University Nijmegen, Netherlands)

Important Dates
---------------

* Submission deadline - 5 May 2008
* Notification of acceptance - 6 June 2008
* Final version - 7 July 2008 (approximately)
* Workshop - 28-29 July 2008

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] Haskell08: Call for papers (co-located w/ ICFP08)

Haskell 08

ACM SIGPLAN 2008 Haskell Symposium
Victoria, British Columbia, Canada
Thursday, 25th September, 2008

FIRST CALL FOR PAPERS

http://haskell.org/haskell-symposium/2008

The Haskell Symposium 2008 is part of the 2008 International Conference
on Functional Programming (ICFP) as an associated ACM SIGPLAN sponsored
symposium.

The purpose of the Haskell Symposium is to discuss experience with
Haskell, and future developments for the language. The scope of the
symposium includes all aspects of the design, semantics, theory,
application, implementation, and teaching of Haskell. Topics of
interest include, but are not limited to, the following:
* Language Design, with a focus on possible extensions and
modifications of Haskell as well as critical discussions of the
status quo;
* Theory, in the form of a formal treatment of the semantics of the
present language or future extensions, type systems, and
foundations for program analysis and transformation;
* Implementations, including program analysis and transformation,
static and dynamic compilation for sequential, parallel, and
distributed architectures, memory management as well as foreign
function and component interfaces;
* Tools, in the form of profilers, tracers, debuggers,
pre-processors, and so forth;
* Applications, Practice, and Experience, with Haskell for scientific
and symbolic computing, database, multimedia and Web applications,
and so forth as well as general experience with Haskell in
education and industry;
* Functional Pearls, being elegant, instructive examples of using
Haskell.

Papers in the latter two categories need not necessarily report
original research results; they may instead, for example, report
practical experience that will be useful to others, re-usable
programming idioms, or elegant new ways of approaching a problem. The
key criterion for such a paper is that it makes a contribution from
which other practitioners can benefit. It is not enough simply to
describe a program!

Before 2008, the Haskell Symposium was known as the Haskell
Workshop. The name change reflects the steady increase of
influence of the Haskell Workshop on the wider community, as well
as an increasing numbers of high quality submissions making the
acceptance process highly competitive. Previously, Haskell
Workshops have been held in La Jolla (1995), Amsterdam (1997),
Paris (1999), Montreal (2000), Firenze (2001), Pittsburgh (2002),
Uppsala (2003), Snowbird (2004), Tallinn (2005),
Portland, Oregon (2006), Freiburg (2007).

Submission Details

* Submission Deadline: Monday, June 23rd 2008
(9:00 am, Samoa Standard Time, UTC -11)
* Author Notification: Friday, July 18th 2008
* Final Papers Due: Monday, July 28th 2008

Submitted papers should be in portable document format (PDF), formatted
using the ACM SIGPLAN style guidelines
(http://www.acm.org/sigs/sigplan/authorInformation.htm). The length is
restricted to 12 pages, and the font size 9pt. Each submission must
adhere to SIGPLAN's republication policy, as explained on the web.
Violation risks summary rejection of the offending submission.

Paper submissions can be made via the easychair webpage

http://www.easychair.org/conferences/?conf=haskell08

Accepted papers will be published by the ACM and will appear in the ACM
Digital Library.

If there is sufficient demand, we will try to organize a time slot for
system or tool demonstrations. If you are interested in demonstrating a
Haskell related tool or application, please send a brief demo proposal
to Andy Gill, andy@galois.com.

Links

* http://haskell.org/haskell-symposium, the permanent homepage of the
Haskell Symposium.
* http://haskell.org/haskell-symposium/2008, the 2008 Haskell
Symposium web page.
* http://www.icfpconference.org/icfp2008, the ICFP 2008 web page.

Program Committee

* Arthur Baars, Instituto Tecnologico de Informatica, Valencia, Spain
* Jeremy Gibbons, Oxford University, UK
* Andy Gill, Galois, USA (Program Chair)
* William Harrison, University of Missouri, Columbia, USA
* Roman Leshchinskiy, University of New South Wales, Australia
* Bernie Pope, University of Melbourne, Australia
* Colin Runciman, University of York, UK
* Tim Sheard, Portland State University, USA
* Mary Sheeran, Chalmers University of Technology, Sweden
* Satnam Singh, Microsoft Research, UK
* Wouter Swierstra, Nottingham University, UK
* Varmo Vene, University of Tartu, Estonia

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] CFP: IWACO 2008

[UPDATE: Date of workshop finalized.]

Call For Papers

International Workshop on Aliasing, Confinement and Ownership

in object-oriented programming (IWACO)

at ECOOP 2008

July 7, 2008, Paphos, Cyprus

www.cs.purdue.edu/homes/wrigstad/iwaco08

The power of objects lies in the flexibility of their

interconnection structure. But this flexibility comes at a cost.

Because an object can be modified via any alias, object-oriented

programs are hard to understand, maintain, and analyse. Aliasing

makes objects depend on their environment in unpredictable ways,

breaking the encapsulation necessary for reliable software components,

making it difficult to reason about and optimise programs, obscuring

the interactions between objects, and introducing security

problems.

Aliasing is a fundamental difficulty, but we accept its presence.

Instead we seek techniques for describing, reasoning about,

restricting, analysing, and preventing the connections between

objects and/or the interactions between them. Promising

approaches to these problems are based on ownership, confinement,

uniqueness, sharing control, escape analysis, argument

independence, read-only references, effects systems, and access

control mechanisms.

The workshop will generally address the question how to manage

interconnected object structures in the presence of aliasing. In

particular, we will consider the following issues (among others):

* models, type and other formal systems, programming language

mechanisms, analysis and design techniques, patterns and

notations for expressing object ownership, aliasing,

confinement, uniqueness, and related topics.

* optimisation techniques, analysis algorithms, libraries,

applications, and novel approaches exploiting object ownership,

aliasing, confinement, uniqueness, and related topics

* empirical studies of programs or experience reports from

programming systems designed with these issues in mind

* novel applications of aliasing management techniques such as

ownership types, ownership domains, confined types, region

types, and uniqueness.

We encourage not only submissions presenting original research

results, but also papers that attempt to establish links between

different approaches and/or papers that include survey material.

Original research results should be clearly described, and their

usefulness to practitioners outlined. Paper selection will be based on

the quality of the submitted material.

The best papers will appear in a special issue of the IET Software

journal.

Program Committee

Peter Müller (Microsoft Research, Chair)

Kevin Bierhoff (Carnegie Mellon University)

John Boyland (University of Wisconsin-Milwaukee)

Werner Dietl (ETH Zurich)

Manuel Fähndrich (Microsoft Research)

Jeff Foster (University of Maryland, College Park)

David Naumann (Stevens Institute of Technology)

Matthew Parkinson (University of Cambridge)

Arnd Poetzsch-Heffter (University of Kaiserslautern)

Mooly Sagiv (Tel-Aviv University)

Tobias Wrigstad (Purdue University)

Important Dates

Submission: April 30, 2008

Notification: May 26, 2008

Final Version: June 9, 2008

Workshop: July 7, 2008

Organisers

Sophia Drossopoulou (Imperial College London)

Dave Clarke (CWI)

James Noble (Victoria University of Wellington)

Tobias Wrigstad (Purdue University)

Participation

The number of participants is limited. Apart from those with accepted

papers, others may attend by sending an email to Peter Müller

(mueller@microsoft.com) indicating what contribution you could make to

the workshop. A small number of places will be reserved for PhD

students and other researchers wishing to begin research in this area.

Selection Process

Both full papers (up to 10 pages) and position papers (1-2 pages) are

welcome. All submissions will be reviewed by the programme committee.

The accepted papers, after rework by the authors, will be published in

the Workshop Proceedings, which will be distributed at the

workshop. All accepted submissions shall remain available from the

workshop web page.

Papers should be sent as PDF files to Peter Müller

(mueller@microsoft.com) by April 27, 2008 and be accompanied by a

text-only message containing: title, abstract and keywords, the

authors' full names, and address and e-mail for

correspondence. Submissions should be in English.

Queries

Queries may be directed to Peter Müller (mueller@microsoft.com).

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs