[TYPES/announce] Legacy of Reuben Goodstein, Friday 14th December, 2012

2012-11-23 Thread S Barry Cooper
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

___

 THE LEGACY OF REUBEN GOODSTEIN

  His Centennial and the Wittgenstein Connection
Friday 14th December 2012, University of Leicester

2012 is the Centenary of the birth of Reuben Louis Goodstein, the first
holder of a UK university chair in Mathematical Logic.

In honour of Goodstein and his legacy, we are organizing a day recognizing
his impact on the development of Mathematical Logic, worldwide, in the UK
and at Leicester.

The list of distinguished speakers includes:

Harvey Rose (Bristol), Jan von Plato (Helsinki), Stanley Wainer (Leeds),
Mathieu Marion/Mitsuhiro Okada (Montreal/Keio, Japan), Mike Price
(Leicester), Mary Walmsley (Leicester).

Topics will include:

* Goodstein's theorem in the light of the Bernays-Goodstein correspondence
* Goodstein sequences and independence of Peano arithmetic
* Goodstein and Wittgenstein
* Goodstein and the Mathematical Association
* We are also hoping to have a panel discussion entitled 'Goodstein
* 'Remembered', where any delegate can share memories and thoughts of
Goodstein.

We anticipate there will be a number of ex-colleagues and students of
Goodstein, and members of the Goodstein family in attendance, and a small
evening dinner for speakers and organisers, and guests.

The meeting is supported by the London Mathematical Society, and there are
a number of bursaries available to UK research students to enable them to
attend the meeting. Registration is free.

To register, and for details of the programme, please go to the meeting
webpage:
http://www2.le.ac.uk/departments/mathematics/legacy-of-goodstein

Download a copy of the conference poster:
http://www2.le.ac.uk/departments/mathematics/legacy-of-goodstein/Goodstein.pdf

__
Organisers: S. Barry Cooper (Leeds), Jeremy Levesley (Leicester), Rick
Thomas (Leicester), Paul Williams (LSE)


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

2012-11-23 Thread Arend Rensink

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

EAPLS PhD Award 2012: Call for Nominations
==
URL: http://eapls.org/pages/phd_award/

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.

Eligibility
---

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 November 2011 – 1 November 2012

Nominations
---

Candidates for the award must be nominated by their supervisor.
Nominating a candidate consists of submitting the thesis to
http://www.easychair.org/conferences/?conf=eaplsphd2012. The
nomination must be accompanied by (a zip file containing)
* a letter from the supervisor describing why the thesis should be
  considered for the award;
* a report from an independent researcher who has acted as examiner
  of the thesis at its defense.
The theses will be evaluated with respect to originality, influence,
relevance to the field and (to a lesser degree) quality of writing.

Procedure
-

The nominations will be evaluated and compared by an international
committee of experts from across Europe. The procedure to be
followed is analogous to the review phase of a conference. The
justification by the supervisor and the external report will play
an important role in the evaluation.

Members of the expert committee are barred from nominating their
own PhD students for the award.

The award consists of a certificate announcing the winner to have
received the EAPLS PhD award 2012. The supervisor will receive a
copy of this certificate. If possible, the certificate will be
handed out ceremonially at a suitable occasion, as for instance
the ETAPS conference.

Apart from the winner, no further ranking of nominees will be
published. The decision of the expert committee is final and
binding, and will not be subject to discussion.

Important dates
---

31 December 2012: Deadline for nominations
21 March 2013:Announcement of the award winner

Expert committee


The Expert committee consists of the following members:
* Mark van den Brand, Universiteit Eindhoven, The Netherlands
* Giorgio Ghelli, University of Pisa, Italy
* Paul Klint, CWI and University of Amsterdam, The Netherlands
* Jens Knoop, Technische Universität Wien, Austria
* Greg Michaelson, Heriot-Watt University , Edinburgh, U.K.
* Arend Rensink, Universiteit Twente, The Netherlands
* Peter Van Roy, Université Catholique de Louvain, Belgium
Further members will be confirmed shortly.


[TYPES/announce] Postdoc position at UIUC in programming languages

2012-11-23 Thread Rosu, Grigore
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Disclaimer: This message does NOT include the word types in it, as requested 
on the types list webpage,
but the successful candidate will also need to define a static semantics of 
C/LLVM.



The Formal Systems Laboratory at UIUC is looking for an excellent postdoc or
researcher to work on the formal K semantics of C/LLVM and/or other low-level
languages.  The semantics will then be used for program analysis and
verification, using the novel matching logic approach and mechanical
translations of K into Coq/Isabelle/ACL2.

If interested, please contact Grigore Rosu (gr...@illinois.edu).

Here are links to related projects and background papers:
K project (http://k-framework.org);
Matching logic (http://matching-logic.org);
Existing C semantics (http://code.google.com/p/c-semantics);
Existing LLVM semantics (https://github.com/davidlazar/llvm-semantics);
popl'12 paper 
(http://fsl.cs.uiuc.edu/index.php/An_Executable_Formal_Semantics_of_C_with_Applications);
oopsla'12 paper: 
(http://fsl.cs.uiuc.edu/index.php/Checking_Reachability_using_Matching_Logic)

Grigore Rosu
Department of Computer Science, University of Illinois at Urbana-Champaign
Email: gr...@illinois.edu, WWW: http://fsl.cs.uiuc.edu/~grosu