[TYPES/announce] Off the Beaten Track 2017: Call for Talk Proposals

[Robert Atkey]

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

# Call for Talk Proposals: Off the Beaten Track 2017

http://conf.researchr.org/track/POPL-2017/OBT-2017

21st January 2017

(co-located with POPL 2017, Paris, France)

## Background

Programming language researchers have the principles, tools,
algorithms and abstractions to solve all kinds of problems, in all
areas of computer science. However, identifying and evaluating new
problems, particularly those that lie outside the typical core PL
problems we all know and love, can be a significant challenge. This
workshop’s goal is to identify and discuss problems that do not often
show up in our top conferences, but where programming language
research can make a substantial impact. We hope fora like this will
increase the diversity of problems that are studied by PL researchers
and thus increase our community’s impact on the world.

While many workshops associated with POPL have become more like
mini-conferences themselves, this is an anti-goal for OBT. The
workshop will be informal and structured to encourage discussion. We
are at least as interested in problems as in solutions.

## Scope

A good submission is one that outlines a new problem or an
interesting, underrepresented problem domain. Good submissions may
also remind the PL community of problems that were once in vogue but
have not recently been seen in top PL conferences. Good submissions do
not need to propose complete or even partial solutions, though there
should be some reason to believe that programming languages
researchers have the tools necessary to search for solutions in the
area at hand. Submissions that seem likely to stimulate discussion
about the direction of programming language research are encouraged.

Use your imagination. It's hard to imagine how a paper that discusses
programming languages could be considered out of scope. If in doubt,
ask the program chair.

## Previous OBTs

2017 marks the sixth year of OBT and its co-location with POPL. The
previous five workshops were:

  - OBT 2016, St. Petersburg, USA
  - OBT 2015, Mumbai, India
  - OBT 2014, San Diego, USA
  - OBT 2013, Rome, Italy
  - OBT 2012, Philadelphia, USA

## Important Dates

  * 10th November 2016: Submission deadline
  * 8th December 2016: Notification
  * (18th December 2016: POPL early registration)
  * 21st January 2017: Workshop

## Submission

Please submit your talk proposal via EasyChair:

https://easychair.org/conferences/?conf=obt2017

All submissions should be in PDF format, two pages or less, in at
least 10pt font, printable on A4 and on US Letter paper. Authors are
welcome to include links to multimedia content such as YouTube videos
or online demos. Reviewers may or may not view linked documents; it is
up to authors to convince the reviewers to do so.

For each accepted submission, one of the authors will give a talk at
the workshop. The length of the talk will depend on the submissions
received and how the program committee decides to assemble the
program.

Reviewing of submissions will be very light. Authors should not expect
a detailed analysis of their submission by the program
committee. Accepted submissions will be posted as is on this web
site. By submitting a document, you agree that if it is accepted, it
may be posted and you agree that one of the co-authors will attend the
workshop and give a talk there. There will be no revision process and
no formal publication.

## Organisers

General chair:

  - Lindsey Kuper, Intel Labs, USA
  Programme chair:

  - Robert Atkey, University of Strathclyde, UK

Programme committee:

  - Ekaterina Komendantskaya, Heriot-Watt University, UK
  - Chris Martens, North Carolina State University, USA
  - Tomas Petricek, University of Cambridge, UK
  - Wren Romano, Google Inc., USA
  - Mary Sheeran, Chalmers University of Technology, Sweden
  - KC Sivaramakrishnan, University of Cambridge, UK
  - Wouter Swierstra, Utrecht University, Netherlands

[TYPES/announce] TOMACS special issue on FORECAST: call for papers

[Michele Loreti]

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

***
*   SPECIAL ISSUE *
*  Formal Methods for the Quantitative Evaluation of  * 
* Collective Adaptive Systems *  
* *
* ACM Transaction on Modeling and Computer Simulation (TOMACS)* 
*  http://tomacs.acm.org/SI-forecast.cfm  *
***


Guest Editors:
* Maurice H. ter Beek, ISTI-CNR, Pisa, Italy
* Michele Loreti, University of Florence, Italy

Submission deadline: 
* January 27, 2017.


Collective Adaptive Systems (CAS) consist of a large number of spatially
distributed heterogeneous entities with decentralised control and
varying degrees of complex autonomous behaviour that may be competing
for shared resources even when collaborating to reach common goals. It
is important to carry out thorough quantitative modelling and analysis
and verification of their design to investigate all aspects of their
behaviour before they are put into operation. This requires combinations
of formal methods and applied mathematics which moreover scale to
large-scale CAS.

In connection with the FORECAST workshop on FORmal methods for the
quantitative Evaluation of Collective Adaptive SysTems, held in Vienna,
Austria on July 8th, 2016, we solicit articles for a special issue of
ACM TOMACS on Formal methods for the quantitative Evaluation of
Collective Adaptive Systems. The primary goal of this special issue is
to raise awareness of the particularities of CAS and the design and
control problems which they bring.

The special issue thus welcomes research papers containing novel,
previously unpublished results in all areas related to Formal Methods
for the Quantitative Evaluation of Collective Adaptive Systems  (on the
crossroads of formal methods, applied mathematics, and software
engineering), including but not limited to the following:
* Qualitative and quantitative modelling techniques and languages for CAS;
* Techniques and tools for verifying, validating, testing and simulating CAS;
* Multi-scale and spatio-temporal modelling and analysis methods for CAS;
* Dependable, reliable and autonomic computing;
* Monitoring and runtime verification of CAS;
* Specification and analysis of socio-technical CAS including smart cities 
  and applications.

We encourage presenters and attendees of FORECAST 2016 to submit an
extended version of their paper to this special issue. We very much also
welcome papers from authors who did not attend. Previously published
papers must contain at least 30%-40% new material to be considered for
the special issue.

The issue is planned to appear during fall 2017. For the editorial
policy, instructions to authors, and further details, please consult the
author guidelines of ACM TOMACS.

When submitting your paper, select the appropriate paper type, Special
Issue on FORECAST, and make sure that you carefully follow the
submission instructions. In the letter to the guest editors please
explain, if your paper is based on a previously published paper, how you
extend the previous publication and describe explicitly the new research
contribution added to the TOMACS submission.

TOMACS is one of the two ACM journals that offer authors the possibility
to have their accepted papers checked for reproducible research results
and reusable and accessible artifacts (see also author guidelines of ACM
TOMACS)  and assign, if successfully evaluated, an according badge to
those (see the result and artifact review and badging policy of ACM). If
you would like your paper to take part in this please say so in your
letter to the guest editors.  

[TYPES/announce] CoqPL 2017: Call for Presentations for the Workshop on Coq for Programming Languages

[Emilio Jesús Gallego Arias]

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

===

  CoqPL 2017

 3rd Workshop on Coq for Programming Languages
  --
  A Coq users and developers meeting
   January 21rd, 2017, co-located with POPL
Paris, France

FINAL CALL FOR PRESENTATIONS

  http://conf.researchr.org/home/CoqPL-2017/
===

Workshop Overview
-

The CoqPL workshop provides an opportunity for programming languages
researchers to meet and interact with one another and members from the
core Coq development team. At the meeting, we will discuss upcoming
new features, see talks and demonstrations of exciting current
projects, solicit feedback for potential future changes, and generally
work to strengthen the vibrant community around our favorite proof
assistant. Topics in scope include:

- General purpose libraries and tactic language extensions

- Domain-specific libraries for programming language formalization and
  verification

- IDEs, profilers, tracers, debuggers, and testing tools

- Experience reports from Coq usage in educational or industrial
  contexts

To foster open discussion of cutting edge research which can later be
published in full conference proceedings, we will not publish papers
from the workshop. However, presentations will be recorded and the
videos made publicly available.

Workshop Format
---

The workshop format will be driven by you, members of the
community. We will solicit abstracts for talks and proposals for
demonstrations and flesh out format details based on responses. We
expect the final program to include experiment reports, panel
discussions, and invited talks (details TBA). Talks will be selected
according to relevance to the workshop, based on the submission of an
extended abstract.

Submission details
--

Submission page: https://easychair.org/conferences/?conf=coqpl2017

Submission:   Friday, October, 14th 2016.
Notification: Friday, November 4th, 2016.
Workshop: Saturday, January 21th, 2017.

Submissions for talks and demonstrations should be described in an
extended abstract, between 1 and 2 pages in length. We suggest
formatting the text using the two-column SIGPLAN latex style (9pt
font) http://www.sigplan.org/Resources/Author/

Program Committee
-

- Lennart BeringerPrinceton University, United States
- Sandrine Blazy  University of Rennes 1, France (Co-Chair)
- Emilio J. Gallego Arias MINES ParisTech, France(Co-Chair)
- Hongjin Liang   University of Science and Technology of China
- Guillaume Melquiond Inria, France
- Benjamin C. Pierce  University of Pennsylvania, United States
- Matthieu Sozeau Inria, France
- Pierre-Yves Strub   École Polytechnique, France

[TYPES/announce] PhD Student Position Opening, Topic: Reactive Synthesis of Graphical User Interface Code, University of Bremen

[Ruediger Ehlers]

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

The "Modelling of Technical Systems" research group at the University of 
Bremen is seeking to hire


1 Ph.D. Student / Scientific Assistant

for the duration of 3 years for a project on *reactive synthesis of 
graphical user interface (GUI) code*, funded by the German Research 
Foundation (DFG). Compensation is based on the German TV-L 13 payscale (full 
position), amounting to approx. EUR 42.000 p.a. (gross). We are seeking 
applicants that already have or are close to the completion of a Master's 
degree in Computer Science or a related subject. As the research project is 
based on automata-theoric foundations and efficient computational engines 
(SAT solvers, SMT solvers, ...), knowledge in these areas is helpful (but 
not strictly needed). The project seeks to develop algorithms for the 
efficient automatic computation of GUI glue code. Such glue code 
orchestrates a program's main functionality with the state and events of its 
graphical user interface. The project is well-suited for writing a Ph.D. 
thesis about the results obtained.


We are a small-sized research group, so the successful applicant can expect 
close collaboration and a high level of support from all other research 
group members. There are no teaching obligations, and no knowledge of German 
is necessary. The (junior) research group is headed by Prof. Rüdiger Ehlers, 
who is happy to answer all questions regarding the project and/or the open 
position.


More details and the official job advertisement can be found at:

http://www.uni-bremen.de/universitaet/die-uni-als-arbeitgeber/offene-stellen/detailansicht/joblist/Job/show/phd-studentscientific-assistant-position-2818.html

The position will remain open until filled. Review of the applications will 
begin on October 19, so prospective applicants are encouraged to apply by 
this date. The official job offer page will remain visible until the end of 
October, but late applications may also be considered. The starting date is 
a bit flexible, but is expected to be in the first quarter of 2017.

[TYPES/announce] Journal of Functional Programming - Call for PhD Abstracts

[Graham Hutton]

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

If you or one of your students recently completed a PhD
in the area of functional programming, please submit the
dissertation abstract for publication in JFP: simple
process, no refereeing, deadline 31st October 2016.

Many thanks,

Graham



CALL FOR PHD ABSTRACTS

Journal of Functional Programming

Deadline: 31st October 2016

http://tinyurl.com/jfp-phd-abstracts



PREAMBLE:

Many students complete PhDs in functional programming each
year.  As a service to the community, the Journal of Functional
Programming publishes the abstracts from PhD dissertations
completed during the previous year.

The abstracts are made freely available on the JFP website,
i.e. not behind any paywall.  They do not require any transfer
of copyright, merely a license from the author.  A dissertation
is eligible for inclusion if parts of it have or could have
appeared in JFP, that is, if it is in the general area of
functional programming.  The abstracts are not reviewed.

Please submit dissertation abstracts according to the instructions
below.  We welcome submissions from both the PhD student and PhD
advisor/supervisor although we encourage them to coordinate.



SUBMISSION:

Please submit the following information to Graham Hutton
 by 31st October 2016.

o Dissertation title: (including any subtitle)

o Student: (full name)

o Awarding institution: (full name and country)

o Date of PhD award: (month and year; depending on the
  institution, this may be the date of the viva, corrections
  being approved, graduation ceremony, or otherwise)

o Advisor/supervisor: (full names)

o Dissertation URL: (please provide a permanently accessible
  link to the dissertation if you have one, such as to an
  institutional repository or other public archive; links
  to personal web pages should be considered a last resort)

o Dissertation abstract: (plain text, maximum 1000 words;
  you may use \emph{...} for emphasis, but we prefer no
  other markup or formatting in the abstract, but do get
  in touch if this causes significant problems)

Please do not submit a copy of the dissertation itself, as
this is not required.  JFP reserves the right to decline
to publish abstracts that are not deemed appropriate.



PHD ABSTRACT EDITOR:

Graham Hutton
School of Computer Science
University of Nottingham
Nottingham NG8 1BB
United Kingdom







This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.

[TYPES/announce] SAFE 2.0 is now available!

[Sukyoung Ryu]

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

Dear all,

We are pleased to announce the official release of SAFE 2.0, a scalable and 
pluggable analysis framework for JavaScript web applications.  General 
information on the SAFE project is available at an invited talk at ICFP 2016:

 https://www.youtube.com/watch?v=gEU9utf0sxE

and the source code and publications are available at:

https://github.com/sukyoung/safe

For more information, please check out a user manual at:

https://github.com/sukyoung/safe/blob/master/manual.pdf

If you have any questions or comments, please feel free to contact the main 
developers of SAFE at safe [ at ] plrg.kaist.ac.kr.

Best,
—
Jihyeok Park, Yeonhee Ryou, and Sukyoung Ryu

[TYPES/announce] TPLP special issue on computational logic for verification

[German Vidal]

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

TPLP-CLV 2016

--
SPECIAL ISSUE OF THEORY AND PRACTICE OF LOGIC PROGRAMMING ON
COMPUTATIONAL LOGIC FOR VERIFICATION

http://tplp-clv.webs.upv.es/
--

The last decade has witnessed a growing interest in the use of 
computational logic methods for program validation and 
verification. For instance, verification problems for imperative 
and object oriented languages can be expressed using Constraint 
Logic Programming (CLP) and related formalisms like Constraint 
Horn Clauses (CHC). Both CLP and CHC have been recently proposed 
as appropriate intermediate languages where program analysis and 
verification techniques for different programming languages can 
be defined, proved correct, and implemented. Furthermore, a 
translation from several programming languages to either CLP or 
CHC already exist, together with efficient methods for solving 
verification problems expressed in these formalisms.

The aim of this special issue is to attract high-quality research 
papers on the interplay between verification techniques and 
computational logic. Topics of interest include, but are not 
limited, to the use of CLP, CHC, and related formalisms for 
program validation and verification. Case studies, system tools 
and challenging problems in this area are also welcome.


SUBMISSION DEADLINE

An expression of interest to submit, title and abstract (to 
gvi...@dsic.upv.es): 
October 15, 2016 (STRICT)

Full paper: November 15, 2016 (TENTATIVE)


SUBMISSION FORMAT

Submissions must be made in the TPLP format 
http://journals.cambridge.org/images/fileUpload/images/tlp_ifc_MAY2014.pdf
and handled by the new TPLP submission system:

- Go to  http://journals.cambridge.org/action/displayJournal?jid=TLP
- Click the button "Submit Your Article" in the left column 
 (register for an account if you don’t have one)
- After you are logged in click "Author Centre" and then 
 "Click here to submit a new manuscript".
- Then choose "Original Article"
- Then, fill the required fields and upload the paper.
 In particular, at the end of the page you’ll see the 
 "Special Issue" option.
 Select "Computational Logic for Verification"


GUEST EDITOR

German Vidal
Universitat Politecnica de Valencia
--

[TYPES/announce] Postdoc/Research fellow position in Formal Methods and System Security, ShanghaiTech University, China

[son...@shanghaitech.edu.cn]

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

[Please accept our apologies if you receive multiple copies]
 
Dear all: 

I am looking for two new members to join my research team at post-doc/research 
fellow level. 

Research topics of particular interest are: 
- Abstract interpretation 
- Binary-code analysis 
- Software and systems security  
- Type systems 
- Model-checking

Your Responsibilities: 
- Conduct research in one or several areas of interest in the field of 
programming languages, software security, and model checking 
- Co-supervise M.S. and Ph.D. students 
- No teaching obligation 

Your profile: 
- Ph.D degree in Computer Science or a relevant field 
- Fluent written and verbal communication skills in English, Chinese is 
optional 
- Strong programming skills 
- An established research record on relevant subjects 

We offer: 
- One year full-time employment contract, extensible up to 3 years 
- Competitive salary and benefits 
- Apartment (low price) 

The application should include: 
- Curriculum citae (including the list of publications and previous positions 
held) 
- Research statement 
- Copies of two representative publications 
- Two letters of reference 

Applications will be considered until the position is filled. 
For further questions about the position, get in touch. 



Dr. Fu SONG 
School of Computer Science and Technology,ShanghaiTech University
Addr: Room 213, H2 Building, No.393 Huaxia Middle Road, Pudong Area Shanghai 
(Temporary)
Tel: +86-(0)21-20685397, +86-15921769918
Website:sist.shanghaitech.edu.cn/faculty/songfu
  

[TYPES/announce] Post-doc: applying verification techniques to consistency in planet-scale storage

[Pierre-Evariste Dagand]

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

[forwarding on behalf of Marc Shapiro ]

In cloud storage systems, which geo-replicate data for performance and
fault tolerance, the CAP theorem points out an inherent trade-off
between consistency and availability: strong consistency provides good
guarantees but is slow and blocks when the network is down; weak
consistency is always available but can expose concurrency anomalies.

The research of the Regal group aims to bridge the gap, thanks to a
“Just-Right Consistency” hybrid approach, aiming to tailor consistency
to the specific requirements of the applications, in order to provide
the highest possible performance and availability at the lowest cost.
Getting this right is difficult: too much synchronisation and the
system crawls to a halt; not enough and data is corrupted.

Therefore, we leverage the CISE static analysis [POPL 2016] to ensure
that the application remains correct, ensuring that (only) the
specific operations that are essential to correctness are
synchronised.

This post-doc aims to consolidate our preliminary results and to
advance the theory and practice of just-right consistency.  Ultimately
our results and tools should be practically available to application
developers. The post-docs shall aim to increase the coverage of the
CISE logic and analysis and to decompose consistency into its
primitive components.  The result of the post-docs will be actual
tools that can be used by application programmers.  This research will
be applied to increasingly demanding, practical large-scale
applications; in particular we shall design, prove correct, implement
and evaluate a petabyte-scale geo-replicated file system and the
applications using it.

Two post-doc positions are potentially available, supported by a joint
research grant with industry (ANR RainbowFS), and by a grant
supporting the productisation of our JRC tools. The research has both
a fundamental and an applied aspect and aims for practical results.
Candidates to these positions should hold a PhD in Computer
Science/Informatics or a related field. They should have an excellent
academic record and experience in distributed systems, distributed
databases, and/or compilation and verification tools. In addition to
research experience, he or she should be a good developer and
experimentor at large scale, and have teamwork and communication
skills. Industrial experience and good knowledge of Erlang and/or
node.js is a plus.

For more information and application procedure, see here:
https://team.inria.fr/regal/job-offers/two-post-doc-positions-practical-just-right-consistency-and-planet-scale-storage/

---
Marc Shapiro, INRIA & LIP6, BC 169  mailto:marc.shap...@acm.org
UPMC, 26-00/211, 4 place Jussieu   http://lip6.fr/Marc.Shapiro/
75252 Paris Cedex 05, France   tél: +33 1 4427 7093
---