[TYPES/announce] PhD/Postdoc vacancy: Homotopy type theory and probabilistic programming

2018-07-03 Thread Bas Spitters
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Aarhus University in Denmark has a PhD and a postdoc vacancy on the
AFOSR funded project:

Homotopy type theory and probabilistic programming

The goal of the project is to use type theory for probabilistic
programming and computer aided proofs in security.

Postdoc:
http://cs.au.dk/about-us/vacancies/scientific-positions/stillinger/Vacancy/show/985804/5283/
Application deadline: 12 august 2018.

PhD:
http://talent.au.dk/phd/scienceandtechnology/opencalls/calls-on-specific-projects/august-2018/type-theory-probabilistic-computation-and-computer-aided-cryptography-proofs/
Application deadline 1 August 2018 at 11.59 PM MET








Related publications include:
* Florian Faissole and Bas Spitters, Synthetic topology in Homotopy
Type Theory for probabilistic programming
http://www.cs.au.dk/~spitters/ProbProg.pdf
* Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters,
Pierre-Yves Strub, Computer-aided proofs for multiparty computation
with active security, CSF https://eprint.iacr.org/2018/502
* Daniel Huang, Greg Morrisett, Bas Spitters, An Application of
Computable Distributions to the Semantics of Probabilistic Programs,
https://arxiv.org/abs/1806.07966


[TYPES/announce] postdoc position at Chalmers | University of Gothenburg

2018-07-03 Thread Thorsten Berger

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

Postdoc position in the area of software variability (with strong ties 
to robotics and embedded/cyber-physical systems). Apply by *July 5*. We 
are looking for a candidate with a good formal background, including 
experiences with Functional Programming, Model-Driven Engineering. and 
Formal Methods.


OVERVIEW

Employment: Fixed-term, 2 years
Extent: 100 % of full time
Location: Department of Computer Science and Engineering / Division of 
Software Engineering, Chalmers | University of Gothenburg

First day of employment: As soon as possible
Applications via: 
https://www.gu.se/english/about_the_university/job-opportunities/vacancies-details/?id=2776

Application deadline: July 5 CEST (strict)


GENERAL INFORMATION

The department of Computer Science and Engineering is jointly hosted by 
Chalmers University of Technology and the University of Gothenburg. It 
is a strongly international department with approximately 80 faculty 
among a total of 260 employees originating from 30 countries. Located in 
Gothenburg -- Sweden’s second-largest city -- the department is 
surrounded by a vibrant ecosystem of software-intensive companies, such 
as Volvo Cars and Volvo AB, Ericsson, ABB, Boeing, and SAAB Aeronautics. 
The department is connected to three science parks in Gothenburg for 
industrial collaborations in fields including intelligent vehicles and 
transport systems, mobile internet, energy, nanotechnology, and life 
sciences. Alumni and members of the department have also created many 
startups, including revolutionary ones such as Spotify.


The announced postdoc position is located at the division of Software 
Engineering. With 21 faculty members it is arguably one of the largest 
software-engineering institutes world-wide, conducting research at the 
highest international level in topics such as model-driven engineering, 
testing, software product lines, empirical software engineering, 
requirements engineering, autonomic computing, and cloud computing. This 
year, the division organizes two of the most influential 
software-engineering conferences, ICSE’18 and SPLC’18. For industrial 
research, the division hosts the Software Center, an associated 
institute with a network of five universities and ten global companies 
including Siemens, Axis, and Jeppesen.



JOB ASSIGNMENTS

The postdoctoral researcher will conduct research in the areas of 
software product-line engineering, model-driven engineering or empirical 
software engineering. The position is embedded into the EU ITEA project 
REVAMP with a focus on re-engineering and migration of variant-rich 
systems into modern and scalable product-line architectures. It is also 
closely related to the EU project Co4Robots where modern variability 
mechanisms (including dynamic variability and adaptation mechanisms) 
will be conceived for robotics and cyber-physical systems. The primary 
job assignment is research, with excellent collaboration opportunities 
with the project partners, including SCANIA, ABB, SAAB, ALTRAN, PAL 
Robotics, and Bosch, among potentially other European partners. The 
position includes 10-20% teaching (negotiable) at the Software 
Engineering division by supervising Master theses and supporting courses 
as a teaching assistant.


Applicants must have a PhD degree in Computer Science, Software 
Engineering or a closely related discipline. Prior publications, 
excellent references, fluency in English as well as good communication, 
collaboration, self-organization, and programming skills are also required.



APPLICATION

Applications are to be written in English and need to contain:
- Cover letter expressing the applicant’s motivation, experiences, and 
relevant qualifications in relation to the announced position
- Detailed curriculum vitae including publications, teaching 
experiences, and three references with their contact details
- Official transcripts of education certificates (degrees, including 
grade reports and other documents when applicable).


Applications only online by July 5 (end of day CEST, strict) via:
https://www.gu.se/english/about_the_university/job-opportunities/vacancies-details/?id=2776

Please contact Thorsten Berger (contact information below) for questions 
about the position.


--
Thorsten Berger
Associate Professor

Department of Computer Science and Engineering
Chalmers | University of Gothenburg, Sweden
http://www.cse.chalmers.se/~bergert
Tel.: +46 (0) 31 772 6075
Mob.: +46 (0) 729 746 246
Skype: tberger.work



[TYPES/announce] Theory and Practice of Differential Privacy (TPDP) 2018 Call for Papers

2018-07-03 Thread Gaboardi, Marco
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Theory and Practice of Differential Privacy (TPDP) 2018 Call for Papers
Colocated with CCS 2018 - October 15 - Toronto, Canada

Differential privacy is a promising approach to privacy-preserving data 
analysis. Differential privacy provides strong worst-case guarantees about the 
harm that a user could suffer from participating in a differentially private 
data analysis, but is also flexible enough to allow for a wide variety of data 
analyses to be performed with a high degree of utility. Having already been the 
subject of a decade of intense scientific study, it has also now been deployed 
in products at government agencies such as the U.S. Census Bureau and companies 
like Apple and Google.

Researchers in differential privacy span many distinct research communities, 
including algorithms, computer security, cryptography, databases, data mining, 
machine learning, statistics, programming languages, social sciences, and law. 
This workshop will bring researchers from these communities together to discuss 
recent developments in both the theory and practice of differential privacy.

Specific topics of interest for the workshop include (but are not limited to): 
– theory of differential privacy,
– privacy preserving machine learning,
– differential privacy and statistics,
– differential privacy and security,
– differential privacy and data analysis,
– trade-offs between privacy protection and analytic utility, 
– differential privacy and surveys,
– programming languages for differential privacy,
– relaxations of the differential privacy definition,
– differential privacy vs other privacy notions and methods, 
– experimental studies using differential privacy,
– differential privacy implementations,
– differential privacy and policy making,
– applications of differential privacy.

Submissions: The goal of TPDP is to stimulate the discussion on the relevance 
of differentially private data analyses in practice. For this reason, we seek 
contributions from different research areas of computer science and statistics. 
Authors are invited to submit a short abstract (2-4 pages maximum) of their 
work. Submissions will undergo a lightweight review process and will be judged 
on originality, relevance, interest and clarity. Submission should describe 
novel works or works that have already appeared elsewhere but that can 
stimulate the discussion between different communities at the workshop. 
Accepted abstracts will be presented at the workshop either as a talk or a 
poster.

The workshop will not have formal proceedings and is not intended to preclude 
later publication at another venue. Please format your submissions according to 
the instructions in https://www. sigsac.org/ccs/CCS2018/papers/. Submissions 
will be accepted at https://easychair.org/ conferences/?conf=tpdp18.

Important dates:

– Abstract submission: July 20 (anywhere on Earth), 
– Author Notification: August 13,
– Workshop: October 15.

Website: http://tpdp.cse.buffalo.edu/2018/

Program committee:

• Aleksandar Nikolov (chair), University of Toronto 
• Raef Bassily, Ohio State University
• Mark Bun, Boston University
• Michael Hay, Colgate University
• Vishesh Karwa, Temple University 
• Katrina Ligett, Hebrew University 
• Anand Sarwate, Rutgers University 
• Thomas Steinke, IBM
• Reza Shokri, National University of Singapore 
• Kunal Talwar, Google





[TYPES/announce] PhD position: Unifying Correctness for Communicating Software

2018-07-03 Thread Jorge A. Perez
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

[Please share widely with potential candidates; apologies for any
cross-postings.]

PHD POSITION ON "UNIFYING CORRECTNESS FOR COMMUNICATING SOFTWARE"
University of Groningen, The Netherlands
Deadline: Tuesday, July 31, 2018.
Contact: Dr. Jorge A. Pérez (j.a.pe...@rug.nl)

This four-year PhD position is embedded in the project "Unifying
Correctness for Communicating Software", a 5-year VIDI career grant
awarded to Dr. Jorge A. Pérez by the NWO (Netherlands Organization for
Scientific Research).

The project will deliver a comprehensive description of how different
verification techniques for message-passing concurrency relate to each
other.
We will use the Curry-Howard correspondence for concurrency (aka
"propositions as sessions") as a reference in formalizing these
relations.
These foundational results will be validated through case studies and
tool prototypes.


The PhD student will contribute to rigorously compare and systematize
different type systems for message-passing programs (such as session
types).
These comparisons will then be used to streamline existing type
systems for message-passing programs, but also to define new type
systems, following the logical foundations defined by the Curry-Howard
correspondence for concurrency.
The research plan for the PhD student can be shaped depending on
his/her strengths and interests.

The PhD student will join a vibrant research group (three PhD students
and a postdoc), supported by generous research funds.
In particular, he or she will work in coordination with a postdoc
researcher (also to be funded by the VIDI career grant), and will have
the chance of visiting international research collaborators to be
involved in the project.


We look for a talented and dedicated student with an MSc degree (or
equivalent) in Computer Science, Logic, or Mathematics, excellent
communication skills in English, and enthusiastic to work in a team.

Candidates with experience in one or more of the following are
especially encouraged to apply:
- semantics of programming languages and/or program verification
- the Curry-Howard isomorphism (aka "propositions as types")
- concurrency theory and/or process calculi
- modal/substructural logics and (their) proof theory

To apply, please send an email to Jorge A. Pérez (j.a.pe...@rug.nl), including:
- a full curriculum vitae;
- a cover letter explaining your motivation to join the project;
- contact information of two references.

Applications received by
Tuesday, July 31, 2018
will receive full consideration; early expressions of interest are encouraged.
The position will remain open until filled; the stating date is flexible.

Further information on the project:
http://www.jperez.nl/vidi

Informal inquiries:
Dr. Jorge A. Pérez (j.a.pe...@rug.nl)

-- 
Jorge A. Pérez
Assistant Professor
Bernoulli Institute for Math, CS and AI
University of Groningen, The Netherlands
URL: http://www.jperez.nl


[TYPES/announce] Deadline Approaching - SBMF 2018

2018-07-03 Thread M.R. Mousavi
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

CALL FOR PAPERS

21st Brazilian Symposium On Formal Methods (SBMF)
Supported by the Brazilian Computer Society (SBC)
Salvador-BA, Brazil
26 to 30 of November 2018
http://www.sbmf2018.ufba.br/


IMPORTANT DATES

(still accepting new abstracts)
Paper Submission Deadline: **July 13th, 2018**
Paper Acceptance Notification: August 28th, 2018
Paper Camera-ready Version: September 4th, 2018

INTRODUCTION

SBMF 2018 is the twenty-first of a series of events devoted to the
development, dissemination, and use of formal methods for the construction
of high-quality computational systems. It is now a well-established event,
with an international reputation.

In 2018, SBMF will take place in Salvador, the capital of the Bahia state,
northeast of Brazil. It is the 3rd city by population in Brazil, with over
2.9 million inhabitants, and it is the second most popular destination in
Brazil for tourists.

SCOPE AND TOPICS

The aim of SBMF is to provide a venue for the presentation and discussion
of high-quality work in formal methods. The topics include (not limited to):

* techniques and methodologies, such as method integration; software and
hardware co-design; model-driven engineering; formal aspects of popular
methodologies; formal design; development methodologies with formal
foundations; software evolution based on formal methods;

* specification and modeling languages, such as well-founded specification
and design languages; formal aspects of popular languages; logic and
semantics for programming and specification languages; code generation;
formal methods of programming paradigms (such as objects, aspects, and
component), formal methods for real-time, hybrid, and safety-critical
systems, formal models of service-oriented, cloud-based, and cyber-physical
systems;

* theoretical foundations, such as domain theory; type systems and category
theory; computational complexity of methods and models; computational
models; term rewriting; models of concurrency, security and mobility;

* verification and validation, such as abstraction, modularization and
refinement techniques; program and test synthesis; correctness by
construction; model checking; theorem proving; static analysis; formal
techniques for software testing; software certification; formal techniques
for software inspection;

* Experience reports regarding teaching formal methods;

* applications, such as experience reports on the use of formal methods;
industrial case studies; tool support.

PAPER SUBMISSION

Papers should present unpublished and original work that has a clear
contribution to the state of the art on the theory and practice of formal
methods. They should not be simultaneously submitted elsewhere.

Papers will be judged by at least three reviewers on the basis of
originality, relevance, technical soundness and presentation quality, and
should contain sound theoretical or practical results. Industry papers
should emphasize practical application of formal methods or report on open
challenges.

Contributions should be written in English and be prepared using Springer?s
Lecture Notes in Computer Science (LNCS) format. Papers may not exceed 16
pages (including figures, references, and appendix). Accepted papers will
be published, after the conference, in a volume of LNCS. Also, a special
issue of Science of Computer Programming (Elsevier) is going to be
published for the very best papers.

Every accepted paper MUST have at least one author registered in the
symposium by the time the camera-ready copy is submitted; the registered
author is also expected to attend the symposium and present the paper.

Papers can be submitted via the following link:
https://easychair.org/conferences/?conf=sbmf2018

ABOUT SALVADOR

Salvador's importance dates back to Brazilian colonization, as it was
established as the country's first capital (founded in 1549). Its center is
a living museum of 17th- and 18th-century architecture and gold-laden
churches. Aside from the many attractions within Salvador (Pelourinho,
Modelo Public Market, Lacerda elevator, Church of Nosso Senhor do Bonfim),
gorgeous coastline lies right outside the city ? a suitable introduction to
the tropical splendor of the state of Bahia.

Salvador presents a vibrant musical scene and popular Carnival
celebrations, being considered one of the birthplaces of Brazilian culture.

KEYNOTE SPEAKERS

Prof. Jose Meseguer (University of Illinois at Urbana-Champaign, USA)

Prof. Alexandre Mota (Federal University of Pernambuco, Brazil)


GENERAL CHAIR

Adolfo Duran (UFBA, Brazil)

PROGRAM COMMITTEE CHAIRS

Mohammad Mousavi (University of Leicester, UK)
Tiago Massoni (UFCG, Brazil)

PROGRAM COMMITTEE (Yet to be confirmed)

Adenilso Sim?o (ICMC/USP, Brazil)
Alexandre Mota (UFPE, Brazil)
Aline Andrade (UFBA. Brazil)
?lvaro Moreira (UFRGS, Brazil)
Ana Cavalcanti (University of York, UK)
Ana de Melo (USP, Brazil)