[TYPES/announce] WST 2016 - Second Call for Papers

[Thiemann, Rene]

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

==
  WST 2016 - 2nd Call for Papers
   15th International Workshop on Termination
   
 September 5-7, 2016, Obergurgl, Austria
http://cl-informatik.uibk.ac.at/events/wst-2016/
==

The Workshop on Termination (WST) traditionally brings together, in an
informal setting, researchers interested in all aspects of termination,
whether this interest be practical or theoretical, primary or derived. The
workshop also provides a ground for cross-fertilization of ideas from term
rewriting and from the different programming language communities. The
friendly atmosphere enables fruitful exchanges leading to joint research
and subsequent publications.

The event is held as part of CLA 2016

  http://cl-informatik.uibk.ac.at/events/cla-2016/

IMPORTANT DATES:
 * submission June 22, 2016
 * notification   July 12, 2016
 * final version  August 3, 2016
 * workshop   September 5-7, 2016

TOPICS: The 15th International Workshop on Termination welcomes
contributions on all aspects of termination and termination analysis.

Contributions from the imperative, constraint, functional, and logic
programming communities, and papers investigating applications of
complexity or termination (for example in program transformation or
theorem proving) are particularly welcome.

Topics of interest include all aspects of termination. This includes
(but is not limited to):
 * certification of termination and complexity proofs
 * challenging termination problems
 * comparison and classification of termination methods
 * complexity analysis in any domain
 * implementation of termination and complexity methods
 * implicit computational complexity
 * infinitary normalization
 * non-termination analysis and loop detection
 * normalization in lambda calculi
 * operational termination of conditional rewrite systems
 * ordinal notation and subrecursive hierarchies
 * SAT, SMT, and constraint solving for (non-)termination analysis
 * scalability and modularity of termination methods
 * termination analysis in any domain
 * well-founded relations and well-quasi-orders

COMPETITION: There will be a live complexity and termination competition
during the workshop, including time to present both the results and the
tools of the participants. More details will be provided in a dedicated
announcement on the competition.

PROGRAM COMMITTEE:
 * Ugo Dal Lago Bologna University
 * Jörg Endrullis   VU University Amsterdam
 * Yukiyoshi Kameyama   University of Tsukuba
 * Salvador Lucas   Universidad Politécnica de Valencia
 * Aart Middeldorp  University of Innsbruck, co-chair
 * Andrey Rybalchenko   Microsoft Research
 * Thomas Ströder   RWTH Aachen
 * René ThiemannUniversity of Innsbruck, co-chair
 * Andreas WeiermannGhent University

INVITED SPEAKERS:
 * Reiner HähnleTU Darmstadt

SUBMISSION: Submissions are short papers/extended abstract which should
not exceed 5 pages. There will be no formal reviewing. In particular, we
welcome short versions of recently published articles and papers submitted
elsewhere. The program committee checks relevance and provides additional
feedback for each submission. The accepted papers will be made available
electronically before the workshop.

Papers should be submitted electronically via the submission page:

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

Final versions should be created using LaTeX and the LIPIcs style file

http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz

[TYPES/announce] PhD student or postdoc position announcement

[Thiemann, Rene]

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

2-year postdoc or 3-year PhD-student position at the University of Innsbruck


The Computational Logic research group at the University of Innsbruck has one
open position funded by the FWF (Austrian science fund) via the START project
„Certifying Termination and Complexity Proofs of Programs“.

The project aims at increasing the reliability in current complexity and
termination provers by independently checking the generated proofs. To this end,
several analysis techniques will be formalized in the theorem prover
Isabelle/HOL, with a focus on term rewriting and Haskell.

For this project, we are looking for an enthusiastic young researcher with a
background in computational logic. Knowledge of automated termination analysis,
complexity analysis, or theorem proving would be an asset.  Candidates with a
strong theoretical background in related areas are also encouraged to apply.
The PhD-student candidate must have a Master's or equivalent degree.  Knowledge
of German is not essential.

The salary is determined by the FWF-funding scheme (3.546,00 EUR monthly 
gross salary for postdocs, and 2.024,90 EUR for PhD-students, cf.
http://www.fwf.ac.at/en/research-funding/personnel-costs/)

Applications (including a CV, a publication list (only for postdocs), and a
letter of recommendation) may be emailed to the project leader René Thiemann
(rene.thiemann at uibk.ac.at) no later than July 6, 2015.

We plan to make decisions on these position until July 10.

The preferred starting date is summer or autumn 2015.

Informal inquiries are also welcome via email.

The city of Innsbruck is superbly located in the beautiful surroundings of the
Tyrolean Alps. The combination of the Alpine environment and urban life in this
historic town provides a high quality of living. 

Further information is available from the following links:

START Project:
http://cl-informatik.uibk.ac.at/research/projects/certifying-termination-and-complexity-proofs-of-pr/

Institute of Computer Science:
http://informatik.uibk.ac.at/

University of Innsbruck:
http://www.uibk.ac.at/

City of Innsbruck:
http://www.innsbruck.at/