[TYPES/announce] VMCAI 2019 Call for Papers

[Constantin Enea]

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

--

  VMCAI 2019

   20th International Conference on Verification, Model 
Checking, and Abstract Interpretation

 Cascais/Lisbon, Portugal, January 13th-January 15th, 2019

   https://popl19.sigplan.org/track/VMCAI-2019 


--

Objective 

VMCAI provides a forum for researchers from the communities of Verification, 
Model Checking, and Abstract Interpretation, facilitating interaction, 
cross-fertilization, and advancement of hybrid methods that combine these and 
related areas. VMCAI 2019 will be the 20th edition in the series. The 
proceedings of the conference will be published in the Advanced Research in 
Computing and Software Science (ARCoSS) subline of the Springer Lecture Notes 
in Computer Science (LNCS) series.

Topics 

VMCAI 2019 welcomes research papers on any topic related to verification, model 
checking, and abstract interpretation. Research contributions can report new 
results as well as experimental evaluations and comparisons of existing 
techniques. Topics include, but are not limited to: 
- Program Verification
- Model Checking
- Abstract Interpretation
- Abstract Domains
- Program Synthesis
- Static Analysis
- Type Systems
- Deductive Methods
- Program Logics
- First-Order Theories
- Decision Procedures
- Interpolation
- Horn Clause Solving
- Program Certification
- Separation Logic
- Probabilistic Programming and Analysis
- Error Diagnosis 
- Detection of Bugs and Security Vulnerabilities
- Program Transformations
- Hybrid and Cyber-physical Systems
- Concurrent Systems
- Analysis of Numerical Properties.

Submissions can address any programming paradigm, including concurrent, 
constraint, functional, imperative, logic, and object-oriented programming.

Paper Submission

Submissions are restricted to 20 pages in Springer’s LNCS format, not counting 
references. Additional material may be placed in an appendix, to be read at the 
discretion of the reviewers and to be omitted in the final version. Formatting 
style files and further guidelines for formatting can be found at the Springer 
website. Papers must describe original work, be written and presented in 
English, and must not substantially overlap with papers that have been 
published or that are simultaneously submitted to a journal or a conference 
with refereed proceedings. Submitted papers will be judged on the basis of 
significance, relevance, correctness, originality, and clarity. They should 
clearly identify what has been accomplished and why it is significant. 
Submissions are handled online: 
https://easychair.org/conferences/?conf=vmcai2019 


Important Dates

- Full paper submission: October 4th, 2018 (anywhere on earth)
- Notification: November 15th, 2018 
- Final version due: November 29th, 2018
- Conference: January 13th-January 15th, 2019

Invited Speakers

- Kedar Namjoshi (Nokia Bell Labs, USA)
- Aditya Nori (Microsoft Research Cambridge, UK)
- Sylvie Putot (Ecole Polytechnique, France)

Program Chairs

- Constantin Enea (University Paris Diderot, France)
- Ruzica Piskac (Yale University, USA)

Program Committee 

- Miltiadis Allamanis (Microsoft Research Cambridge, UK)
- Timos Antonopoulos (Yale University, USA)
- Domagoj Babic (Google Inc., USA)
- Josh Berdine (Facebook, UK)
- Ahmed Bouajjani (University Paris Diderot, France)
- Patrick M. Cousot (New York University, USA)
- Cezara Drăgoi (INRIA Paris, France) 
- Constantin Enea (University Paris Diderot, France)
- Javier Esparza (TU Munich, Germany)
- Jerome Feret (INRIA Paris, France) 
- Khalil Ghorbal (INRIA Rennes, France)
- Roberto Giacobazzi (University of Verona, Italy, and IMDEA Software 
Institute, Spain)
- Alberto Griggio (Fondazione Bruno Kessler, Italy)
- Jan Kretinsky (TU Munich, Germany)
- K Narayan Kumar (Chennai Mathematical Institute, India)
- Ori Lahav (Tel Aviv University, Israel)
- Anthony Widjaja Lin (Oxford University, UK)
- Ruben Martins (Carnegie Mellon University, USA)
- Kedar Namjoshi (Nokia Bell Labs, USA)
- Dejan Nickovic (Austrian Institute of Technology, Austria)
- Jens Palsberg (University of California, Los Angeles, USA)
- Ruzica Piskac (Yale University, USA)
- Sylvie Putot (Ecole Polytechnique, France)
- Daniel Schwartz-Narbonne (Amazon, USA)
- Martina Seidl (Johannes Kepler University, Austria)
- Sharon Shoham (Tel Aviv University, Israel)
- Caterina Urban (ETH Zurich, Switzerland)
- Lenore Zuck (University of Illinois at Chicago, USA)
- Damien Zufferey (MPI-SWS, Germany)

[TYPES/announce] DICE Special Issue in TCS -- 2nd Call for Papers

[Martin Avanzini]

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



==

Call for Papers

THEORETICAL COMPUTER SCIENCE
Special Issue on Implicit Computational Complexity
(open post-conference publication of the workshops DICE 2016, 2017
 and 2018)

Deadline: October 12th 2018

Guest Editors:
 Martin Avanzini 
 Romain Péchoux 

==


The area of Implicit Computational Complexity has grown from several proposals
for using logic and formal methods to provide languages for complexity-bounded
computation (such as polynomial time, polynomial space or logarithmic space
computation). Its aim is to study computational complexity without reference to
external measuring conditions or particular machine models, but only in terms of
language restrictions or logical/computational principles implying complexity
properties.

We welcome contributions on various aspects of Implicit Computational 
Complexity,
including (but not exclusively) the following topics:
 - types for controlling / inferring / checking complexity
 - logical systems for implicit computational complexity
 - programming languages for complexity bounded computation
 - logics closely related to complexity classes
 - static resource analysis and practical applications
 - semantics of complexity-bounded computation
 - application of implicit complexity to security
 - rewriting and termination orderings
 - termination and resource analysis for probabilistic programs
 - semantic methods to analyse resources

This special issue of Theoretical Computer Science follows the informal
workshops on Developments in Implicit Computational Complexity (DICE), DICE 2016
in Eindhoven (http://lipn.univ-paris13.fr/DICE2016/), DICE 2017 in Uppsala
(http://cbr.uibk.ac.at/events/dice-fopara/) and DICE 2018 in Thessaloniki
(http://cl-informatik.uibk.ac.at/users/zini/events/dice18).

Submission to this special issue is open to everyone, including those who did
not participate in the above editions of DICE.

DICE workshops have been held annually as satellite events of ETAPS: DICE 2010
in Paphos, DICE 2011 in Saarbrücken, DICE 2012 in Tallinn, DICE 2013 in Rome,
DICE 2014 in Grenoble, DICE 2015 in London, DICE 2016 in Eindhoven, DICE 2017 in
Uppsala and DICE 2018 in Thessaloniki. Previous post-conference publications
have appeared in
 - Information & Computation for DICE 2011,
 - Theoretical Computer Science for DICE 2012,
 - Information & Computation for DICE 2013,
 - Information & Computation for DICE 2014 & 2015.

More information on the DICE workshop series is available at:

http://perso.ens-lyon.fr/patrick.baillot/DICE

Theoretical Computer Science solicits high quality papers reporting research
results related to the topics mentioned above. All papers must be original,
unpublished, and not submitted for publication elsewhere. All manuscripts and
any supplementary material should be submitted through Elsevier Editorial System
(EES). The authors must select as “SI:DICE” when they reach the “Article Type”
step in the submission process. The EES submission website is located at:

http://ees.elsevier.com/tcs/default.asp

All papers will be peer-reviewed by three independent reviewers. Requests for
additional information should be addressed to the guest editors. A detailed
submission guideline is available as “Guide to Authors” at:

http://www.journals.elsevier.com/theoretical-computer-science

Submissions must be submitted no later than October 12th 2018. We are aiming
for a turnaround of no more than eight months.

[TYPES/announce] ERC "RustBelt" project: Postdoc and PhD student positions available at MPI-SWS

[Derek Dreyer]

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

I am pleased to announce the availability of multiple postdoc and PhD
student positions in my research group at the Max Planck Institute for
Software Systems (MPI-SWS), funded by a 2015 ERC Consolidator Grant
for the project "RustBelt: Logical Foundations for the Future of Safe
Systems Programming".

http://plv.mpi-sws.org/rustbelt

This 5-year project (which began in April 2016) concerns the
development of rigorous formal foundations for the Rust programming
language.  The project summary appears at the bottom of this message.

Although the main high-level goal of the project is to build logical
foundations for the Rust programming language -- see our POPL'18 paper
-- the project also serves to fund technical work on two other major
research efforts that feed into the main goal:

1. The development of *Iris*, a simplifying and unifying framework for
higher-order concurrent separation logic in Coq [POPL'15, ICFP'16,
POPL'17, ESOP'17, ICFP'18, JFP'18].  See the Iris web page at
http://iris-project.org/ for further details.

2. Our ongoing study of improved semantics and logics for relaxed
memory models (see e.g. our work on the separation logic GPS
[OOPSLA'14, PLDI'15, ECOOP'17] and the "promising" semantics for
solving the out-of-thin-air problem [POPL'17, ECOOP'17, ESOP'18]).

*POSTDOCS*: I am seeking exceptional candidates with a strong,
internationally competitive track record of research in programming
languages and/or verification.  The primary criterion is quality, but
I am particularly interested in candidates who have specialized
expertise in one or more of the following areas:

- Rust
- substructural/ownership type systems
- verification of concurrent programs
- weak/relaxed memory models
- interactive theorem proving in Coq
- compiler verification

Experience programming in Rust is a welcome bonus, but not required.

*STUDENTS*: I am seeking exceptional candidates who have at least some
background in programming language theory and/or formal methods, and
who are eager to work on deep foundational problems with the potential
for direct impact on a real, actively developed language.  A
bachelor's or master's degree is required.  For more details about the
MPI-SWS graduate program, see here:
https://www.mpi-sws.org/graduate-studies/.

Successful applicants will join the Foundations of Programming group,
led by me at the Max Planck Institute for Software Systems (MPI-SWS)
in Saarbruecken, Germany.  Current and former postdocs in the group
have included Andreas Rossberg (co-designer of WebAssembly), Chung-Kil
Hur, Neel Krishnaswami, Aaron Turon (manager of the Rust project at
Mozilla), Jacques-Henri Jourdan, Ori Lahav, Pierre-Marie Pédrot, and
Azalea Raad.  Current and former PhD students in the group have
included Georg Neis, Beta Ziliani, Scott Kilpatrick, David Swasey,
Ralf Jung, Jan-Oliver Kaiser, Hoang-Hai Dang, Marko Doko, and
@pythonesque.  The RustBelt project benefits from longstanding active
collaborations with Viktor Vafeiadis (MPI-SWS), Lars Birkedal (Aarhus
University), Chung-Kil Hur & Jeehoon Kang (Seoul National University),
Deepak Garg (MPI-SWS), and Robbert Krebbers (TU Delft), as well as the
many contributors to the Iris project (http://iris-project.org).

The working language at MPI-SWS is English.

*Application deadline*: OCTOBER 31.  If you are interested in joining
the RustBelt team and want to learn more about the project, please
contact me directly at dre...@mpi-sws.org.  To apply for a postdoc (or
PhD student) position, please submit a CV (and/or grade transcript),
research statement (or statement of purpose), and list of references
to https://apply.mpi-sws.org.  If you are unable to apply by the
deadline but are interested in a position, please contact me anyway.

For further information, see the project web page at:
http://plv.mpi-sws.org/rustbelt/

Best regards,
Derek Dreyer



Summary of the RustBelt project proposal:

A longstanding question in the design of programming languages is how
to balance safety and control.  C-like languages give programmers
low-level control over resource management at the expense of safety,
whereas Java-like languages give programmers safe high-level
abstractions at the expense of control.

Rust is a new language developed at Mozilla Research that marries
together the low-level flexibility of modern C++ with a strong
"ownership-based" type system guaranteeing type safety, memory safety,
and data race freedom.  As such, Rust has the potential to
revolutionize systems programming, making it possible to build
software systems that are safe by construction, without having to give
up low-level control over performance.

Unfortunately, none of Rust's safety claims have been formally
investigated, and it is not at all clear that they hold.  To rule out
data races and other common programming errors, Rust's core type
system