Sergio Maffeis | 1 Nov 11:07 2010

[TYPES/announce] PhD Studentship in Foundations of Secure Web Programming at Imperial College London

[ The Types Forum (announcements only), ]

*** PhD Studentship in Foundations of Secure Web Programming ***
*** Imperial College London ***

We are looking for a student with a top degree from a good university
and a strong interest in some of these topics:
- formal semantics of programming languages;
- theorem provers and proof assistants;
- static analysis and type systems;
- web security.

Starting date is as soon as possible. Applications will be considered on
an ongoing basis until December 31st, 2010.

The PhD Studentship consists of a 3 years tax free bursary of £15,590
per annum, plus UK/EU tuition fees and an allowance for equipment and
academic travel costs.

For further information please contact Dr. Sergio Maffeis:

Tobias Wrigstad | 3 Nov 00:20 2010

[TYPES/announce] STOP'11 CFP -- Extended Deadline Nov 8th

[ The Types Forum (announcements only), ]

	     **** Deadline extended to Nov. 8th ****

                       Call for Papers
              Script to Program Evolution (STOP)
                         at POPL 2011
                  Jan 29th, 2011, Austin, TX

Recent years have seen increased use of scripting languages in
large applications. Scripting languages optimize development time,
especially early in the software life cycle, over safety and

As the understanding of the system reaches a critical point and
requirements stabilize, scripting languages become less appealing.
Compromises made to optimize development time make it harder to
reason about program correctness, harder to do semantic-preserving
refactorings, and harder to optimize execution speed. Lack of type
information makes code harder to navigate and to use correctly. In
the worst cases, this situation leads to a costly and potentially
error-prone rewrite of a program in a compiled language, losing
the flexibility of scripting languages for future extension.

Recently, pluggable type systems and annotation systems have been
proposed.  Such systems add compile-time checkable annotations
without changing a program's run-time semantics which facilitates
early error checking and program analysis.  It is believed that
untyped scripts can be retrofitted to work with such systems.
(Continue reading)

Martin Hofmann | 3 Nov 08:15 2010

[TYPES/announce] 3 years research assistant position in TCS, LMU Munich

[ The Types Forum (announcements only), ]

A position for a research assistant in a DFG project is

Project title: Pointers as an abstract data type:
complexity-theoretic and programming-language aspects (PURPLE)

Investigators: Martin Hofmann and Ulrich Schöpp

Duration: 36 months

Start date: as soon as possible but not later than June 2011.

Remuneration: German scale 13 TV-L (38k-54k EUR according to age,
experience, family status)

Background: PhD in theoretical informatics with some topical overlap,
see project description. Candidates with an excellent Diploma or
Master in this area are also encouraged to apply; in this case
the project work may lead to a PhD.

Location: The project will be carried out at the Institute for
Informatics of Ludwig-Maximilians-Universität Munich, Germany.
LMU is an equal opportunities employer.

Applications should be sent by E-Mail to Sigrid Roden
roden@... as a single PDF file containing in particular CV,
research statement, and the names of two potential referees. There is
(Continue reading)

Alain Girault | 3 Nov 23:05 2010

[TYPES/announce] MEMOCODE 2011 Call for Papers

[ The Types Forum (announcements only), ]

MEMOCODE 2011 Call for Papers

The ninth ACM-IEEE* International Conference on Formal Methods and
Models for Codesign (MEMOCODE 2011) will be held on July 11-13, 2011
in Microsoft Research Cambridge, UK.



Abstract submission deadline: February 25, 2011
Paper submission deadline:    March 4, 2011
Notification of acceptance:   April 29, 2011
Final Version for Papers:     May 13, 2011
Poster submission deadline:   May 13, 2011
Notification for Posters:     May 27, 2011


The ninth MEMOCODE conference will attract researchers and
practitioners who create methods, tools, and architectures for the
design of hardware/software systems.  These systems face increasing
design complexity including tighter constraints on timing, power,
costs, and reliability. MEMOCODE seeks submissions that present novel
formal methods and design techniques addressing these issues to
(Continue reading)

Marieke Huisman | 4 Nov 15:53 2010

[TYPES/announce] PhD and Post Doc position on ERC project Verifcation of Concurrent Data Structures (U. Twente, Netherlands)

[ The Types Forum (announcements only), ]

The research group
    Formal Methods and Tools
at the
    University of Twente
    (Enschede - The Netherlands)
is looking for a
    PhD researcher (4 years)
and a
    post doc researcher (3 years),
to work on the 5 year research project

    VerCors (Verification of Concurrent Data Structures),

funded by the European Research Council.

The PhD student will work in particular on:
   The specification and Verification of Concurrent Data Structures
   with different Locking Policies

The post doc researcher will work in particular on:
   User-friendly specification and automated verification of
   concurrent data structures

Our research:

Goal of the VerCors project is to develop a general specification and
(Continue reading)

retore | 4 Nov 22:54 2010

[TYPES/announce] logic, categories, semantics - Bordeaux 12-13 nov.

[ The Types Forum (announcements only), ]

Dear colleagues, 

Here is a colloquium on logic, categories and formal semantics. 
We have 8 places left (if there are extra participants, they possibly will have to take care of their lunches). 
Registration is free, but the program below is worth a visit to Bordeaux. 

Best regards, 
Christian Retoré

international colloquium organised by Jean Gillibert & Christian Retoré (IMB, INRIA, LABRI) 
under the auspices of the French Mathematical Society (SMF)

12 AND 13 NOVEMBRE 2010
Salle de conférences 
Institut de Mathématiques de Bordeaux Bât. A33 
Université Bordeaux 1, 
351 cours de la Libération 33405 Talence,


08:45 - 08:55  Présentation (Jean Gillibert, Christian Retoré)
09:00 - 09:40  Pierre Cartier (IHES, Orsay)   
09:45 - 10:25 Jean-Yves Girard (CNRS, IML, Marseille) 
Interdire ou réfuter ? Le statut ambigu de la normativité
11:00 - 11:40   Nicholas Asher (CNRS, IRIT, Toulouse)
A web of words 
11:45 - 12:25  Steve Vickers (University of Birmingham) 
Aspects of geometric logic   
14:00-14:40  Thomas Streicher (Technische Universität Darmstadt) 
Christiano Braga | 5 Nov 14:01 2010

[TYPES/announce] SBLP 2011: Call For Papers

[ The Types Forum (announcements only), ]

[Apologies for multiple copies of this call.]

SBLP 2011: Call For Papers

15th Brazilian Symposium on Programming Languages

Sao Paulo, Brazil
September 26-30, 2011


Paper abstract submission (15 lines): April 22nd, 2011
Full paper submission: April 29th, 2011
Notification of acceptance: May 30th, 2011
Final papers due: July 29th, 2011


Gary T. Leavens, Univ. of Central Florida
Jose Luis Fiadeiro, Univ. of Leicester


The 15th Brazilian Symposium on Programming Languages, SBLP 2011, will
be held in Sao Paulo, Brazil, between September 26th and 30th,
2011. SBLP provides a venue for researchers and practitioners
(Continue reading)

carlos.martin | 7 Nov 12:46 2010

[TYPES/announce] LATA 2011: 2nd call for papers

[ The Types Forum (announcements only), ]


2nd Call for Papers


Tarragona, Spain, May 30 – June 3, 2011



LATA is a yearly conference in theoretical computer science and its applications. Inheriting the
tradition of the International PhD School in Formal Languages and Applications that was developed at
Rovira i Virgili University in the period 2002-2006, LATA 2011 will reserve significant room for young
scholars at the beginning of their career. It will aim at attracting contributions from both classical
theory fields and application areas (bioinformatics, systems biology, language technology,
artificial intelligence, etc.).


Topics of either theoretical or applied interest include, but are not limited to:

- algebraic language theory
- algorithms for semi-structured data mining
(Continue reading)

Arend Rensink | 9 Nov 15:06 2010

[TYPES/announce] EAPLS PhD Award 2010: Call for Nominations

[ The Types Forum (announcements only), ]

EAPLS PhD Award 2010: Call for Nominations

The European Association for Programming Languages and Systems
has established a Best Dissertation Award in the international
research area of programming languages and systems. The award
will go to the PhD student who in the previous period has made
the most original and influential contribution to the area. The
purpose of the award is to draw attention to excellent work, to
help the career of the student in question, and to promote the
research field as a whole.


Eligible for the award are those who successfully defended their PhD
* at an academic institution in Europe
* in the field of Programming Languages and Systems
* in the period from 1 January 2009 – 1 November 2010


Candidates for the award must be nominated by their supervisor.
Nominating a candidate consists of submitting the thesis to The
(Continue reading)

Valeria de Paiva | 15 Nov 00:41 2010

[TYPES/announce] IMLA11: Call for Papers

[ The Types Forum (announcements only), ]

                  Fifth International Workshop on
             Intuitionistic Modal Logic and Applications


 A 14th Logic, Methodology and Philosophy of Science affiliated workshop
                           Nancy, France, July, 2011

Constructive modal logics and type theories are of increasing
foundational and practical relevance in computer science. Applications
are in type disciplines for programming languages, and meta-logics for
reasoning about a variety of computational phenomena.

Theoretical and methodological issues center around the question of how
the proof-theoretic strengths of constructive logics can best be
combined with the model-theoretic strengths of modal logics. Practical
issues center around the question which modal connectives with
associated laws or proof rules capture computational phenomena
accurately and at the right level of abstraction.

This workshop will bring together designers, implementers, and users to
discuss all aspects of intuitionistic modal logics and type theories.
Topics include, but are not limited to:

* applications of intuitionistic necessity and possibility
* monads and strong monads
(Continue reading)