[TYPES/announce] APLAS 2012: Call for Posters and Demos

2012-09-07 Thread Kohei SUENAGA
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

(Apologies for multiple copies.)

   10th Asian Symposium on
  Programming Languages and Systems
 (APLAS 2012)
  Call for Poster and Demos

APLAS 2012 will include a poster and demo session during the
conference. The poster session aims to give students and professionals
an opportunity to present technical materials to the research
community, and to get responses from other researchers in the field.

This year, accepted posters will be presented in the main hall so that
presenters have much opportunity of discussion during breaks. Standing
by the poster on each break is not mandatory, though.

* Scope

Poster and demo contributions are sought in all areas of programming
languages and systems, including the following topics:

- semantics, logics, foundational theory;
- design of languages and foundational calculi;
- type systems;
- compilers, interpreters, abstract machines;
- program derivation and transformation;
- program analysis, verification, model-checking, software security;
- concurrency, constraints, domain-specific languages;
- tools for programming, verification, implementation.

* Format of Posters

A space of A1 paper size (594 mm wide and 841 mm high) will be
provided for each presentation. AC Power outlet of 100V will be also
provided during the poster  demo session. If you need more space and
facilities, contact the poster chair (aplas2012-poster AT
fos.kuis.kyoto-u.ac.jp).

* Submission

Each presenter should e-mail a 1-2 page abstract in PDF to the poster
chair (Kohei Suenaga: aplas2012-poster AT fos.kuis.kyoto-u.ac.jp) by
October 5th 2012. The abstract should include the title, author(s),
affiliation(s) and summary of the work. The program of the poster
session will be announced by October 29th, 2012. We hope to
accommodate every poster, but may restrict presentations (based on
relevance and interest to the community) due to space constraints.

* Important Dates

Submission deadline: October 5th, 2012
Notification: October 29th, 2012

* Contact

Poster chair: Kohei Suenaga
(aplas2012-poster AT fos.kuis.kyoto-u.ac.jp)


[TYPES/announce] Software Verification and Testing Track at ACM SAC 2013: last CfP

2012-09-07 Thread Jun PANG
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

==
28th Annual ACM Symposium on Applied Computing
Software Verification and Testing Track
March 18 - 22, 2013, Coimbra, Portugal

(Proceedings published by ACM, Selected papers invited to a special
issue of Science of Computer Programming)

More information:
http://www.win.tue.nl/sacsvt13/ and
http://www.acm.org/conferences/sac/sac2013/
===

Important dates
---
* September 21st 2012: Submission deadline
* November 10th 2012: Notification of acceptance/rejection
* November 30th 2012: Camera-ready versions due


ACM Symposium on Applied Computing
--
The ACM Symposium on Applied Computing (SAC) has gathered scientists
from different areas of computing over the past twenty-seven
years. The forum represents an opportunity to interact with different
communities sharing an interest in applied computing.

SAC 2013 is sponsored by SIGAPP and will be held at the Institute of
Engineering of the Polytechnic Institute of Coimbra, Coimbra,
Portugal.


Software Verification and Testing Track
---
We invite authors to submit new results in formal verification and
testing, as well as development of technologies to improve the
usability of formal methods in software engineering. Also welcome are
detailed descriptions of applications of mechanical verification to
large scale software. Possible topics include, but are not limited to:

- tools and techniques for verification of large scale software systems
- real world applications and case studies applying software verification
- static and run-time analysis
- abstract interpretation
- model checking
- theorem proving
- refinement and correct by construction development
- model-based testing
- verification-based testing
- run-time verification
- symbolic execution and partial evaluation
- analysis methods for dependable systems
- software certification and proof carrying code


Submissions guidelines
--
Paper submissions must be original, unpublished work. Submissions
should be in electronic format, via the START site:
https://www.softconf.com/c/sac2013/. Author(s) name(s) and address(es)
must not appear in the body of the paper, and self-reference should be
avoided and made in the third person. Submitted paper will undergo a
blind review process. Authors of accepted papers should submit an
editorial revision of their papers that fits within six two-column
pages (an extra two pages, to a total of eight pages, may be available
at a charge). Please comply to this page limitation already at
submission time. Accepted papers will be published in the ACM SAC
2013 proceedings.

For accepted papers, registration for the conference is required and
allows accepted papers to be printed in the conference
proceedings. The accepted paper MUST be presented by an author or a
proxy. This is a requirement for the paper to be part of the ACM/IEEE
digital library.

A special issue of Science of Computer Programming (SCP) has been
confirmed. Selected papers will be invited for submission, and will be
peer-reviewed according to the standard policy of SCP.

(New for SAC 2013) Student Research Competition (SRC) Program:
Graduate students are invited to submit research abstracts (minimum of
2-page and maximum of 4-page) following the instructions published at
SAC 2013 website. Submission of the same abstract to multiple tracks
is not allowed. All research abstract submissions will be reviewed by
researchers and practitioners with expertise in the track focus area
to which they are submitted. Authors of selected abstracts will have
the opportunity to give poster presentations of their work and compete
for three top-winning places. The SRC committee will evaluate and
select First-, Second-, and Third- place winners. The winners will
receive cash awards and SIGAPP recognition certificates during the
conference banquet. Authors of selected abstracts are eligible to
apply to the SIGAPP Student Travel Award program for support.


Program committee
-
Wan Fokkink, Vrije Universiteit Amsterdam, The Netherlands
Sarfraz Khurshid, University of Texas at Austin, USA
Ramtin Khosravi, University of Tehran, Iran
Keqin Li, SAP Research, France
Yang Liu, National University of Singapore, Singapore
Delphine Longuet, Universite Paris-Sud 11, France
Yves Le Traon, University of Luxembourg, Luxembourg
MohammadReza Mousavi (co-chair), Eindhoven University of Technology,
The Netherlands
Mercedes Merayo, Universidad Complutense de Madrid, Spain
Stephan Merz, INRIA Nancy, France
Markus Mueller-Olm, University of Muenster, Germany
Jun Pang (co-chair), University of Luxembourg, Luxembourg
Dave Parker, University of Birmingham, UK
Hongyang Qu, Oxford University, UK
Martin Steffen, University of Oslo, Norway
Tim 

[TYPES/announce] Book Announcement

2012-09-07 Thread Gopalan Nadathur
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dale Miller and I are happy to announce the recent publication of our
book entitled Programming with Higher-Order Logic by Cambridge
University Press. The table of contents and other details about the
book can be found at https://sites.google.com/site/proghol/.

The book argues for using higher-order intuitionistic logic as the
foundations of logic programming. In elaborating this argument, the
book presents
  - a sequent calculus based characterization of logic programming;
  - a proof search approach to computation;
  - higher-order logic programming;
  - polymorphic typing;
  - modular programming and abstract data types; and
  - simply-typed lambda-terms and their unification.

The book also emphasizes the practical application of higher-order
logic programming by showing that it can be used to provide elegant
formalizations and implementations of computations that manipulate
bindings in syntax.  In addition to a general exposition of this
approach, individual chapters present extended examples relating to
  - implementing proof systems,
  - computing with functional programs, and
  - encoding the pi-calculus.

The lambda Prolog language is used to illustrate the underlying
computation-related ideas and their applications. The website for the
book provides all the lambda Prolog code used in the book. The reader
can experiment with this code using the Teyjus system available from
http://teyjus.cs.umn.edu/.