[TYPES/announce] 4 year PhD position in Innsbruck (application deadline: 27 May 2020)

[Aart Middeldorp]

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

The University of Innsbruck invites applications for a 4 year PhD position
in the Computational Logic research group. Candidates must hold a master
degree in computer science or mathematics. Knowledge of term rewriting and
automated deduction is desired. Candidates close to obtaining a master degree
are also invited to apply. Knowledge of German is not required. The position
is an official university position with 15 September 2020 as starting date.
The main task will be to pursue research leading to a dissertation. The
position comes with teaching obligations of 2 hours per semester. The minimum
gross salary (stipulated by collective agreement) for this position amounts
to € 1.465 per month (14 times).

The official job advert (code MIP-11245) appeared at

http://orawww.uibk.ac.at/public/karriereportal.details?asg_id_in=11245

Applications (including CV, list of presentations, motivation letter, possible
research topics) must be submitted electronically at

https://orawww.uibk.ac.at/public/karriereportal.bewerben?page=w_id=11245

We look forward to receiving your online application (code MIP 11245) until

May 27, 2020

Informal inquiries may be addressed to

aart.middeldorp at uibk.ac.at

The city of Innsbruck, which hosted the Olympic Winter Games in 1964 and 1976,
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:

Computational Logic:
http://cl-informatik.uibk.ac.at/

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

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

[TYPES/announce] Verification Mentoring Workshop 2020: Call for scholarship applications

[Jean-Baptiste Jeannin]

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

Verification Mentoring Workshop (VMW 2020)
http://i-cav.org/2020/mentoring/

co-located with CAV 2020
20 July 2020
Los Angeles, California, USA

APPLICATIONS FOR SCHOLARSHIPS

We warmly invite eligible students to apply for scholarships to attend the
Verification Mentoring Workshop and CAV.  The deadline for applications is
May 15, 2020. Applications are received via the form at
https://forms.gle/5Nk61at9juHqVTDL8

ABOUT VMW

The purpose of the Verification Mentoring Workshop is to provide mentoring
and career advice to early-stage graduate students, to attract them to
pursue research careers in the area of computer-aided verification. The
workshop will particularly encourage participation of women and
underrepresented minorities.

The workshop program will include a number of talks and interactive
sessions. The talks will give an overview of the field along with brief
introductions to the varied topics highlighted at CAV 2020. Other talks
will provide mentoring and career advice, from academia and industry.
More information can be found at http://i-cav.org/2020/mentoring/

Please note that the scholarships this year may not cover travel, depending
on how the current situation evolves. All students interested in attending
VMW 2020 should still apply for scholarships and watch
http://i-cav.org/2020/mentoring/ for further updates.

SPEAKERS

Erika Ábrahám, RWTH Aachen University
Rajeev Alur, University of Pennsylvania
Eva Darulova, MPI-SWS
Ranjit Jhala, University of California, San Diego
Rupak Majudar, MPI-SWS
Ken McMillan, Microsoft Research

In case of questions, please contact the organizers

Roopsha Samanta (chair) 
Rayna Dimitrova 
Jean-Baptiste Jeannin 
James R. Wilcox 

[TYPES/announce] Online seminars in functional programming @ Chalmers

[Benjamin C. Pierce]

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

The folks at Chalmers have just put together an online seminar series in 
Functional Programming—details here: http://chalmersfp.org 
. It’s open to the public, and it looks like it should 
have quite broad appeal. First seminar is Simon PJ, next Monday!
 
See you there!

   - Benjamin

[TYPES/announce] Call for participation, LangSec 2020, May 21st, on Zoom

[Gang (Gary) Tan]

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

Call for Participation
Sixth Workshop on Language-Theoretic Security (LangSec)
Affiliated with 41st IEEE Symposium on Security and Privacy (Oakland)
May 21st, 2020. On Zoom.

LangSec was founded to bring together researchers who were interested
in the language-theoretic approach to software security (LangSec).  We
are glad to announce the program of LangSec 2020, featuring two
keynotes by David Walker from Princeton University and Jeremy Yallop
from University of Cambridge. The full program also includes two
invited talks and a number of technical talks, with detailed
information at the following website:

http://spw20.langsec.org/workshop-program.html

Registration fee for general attendance (including the full IEEE S
conference and all workshops) is only $25:

http://spw20.langsec.org/registration-info.html

--

Gang (Gary) Tan
Associate Professor
Penn State CSE and ICS
W358 Westgate Building
http://www.cse.psu.edu/~gxt29
Tel:814-8657364

[TYPES/announce] FMBC 2020: 2nd Workshop on Formal Methods for Blockchains (3rd CfP, Deadline Extension)

[Bruno Bernardo]

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

[ Please distribute, apologies for multiple postings. ]



2nd Workshop on Formal Methods for Blockchains (FMBC) 2020 - Third Call

https://fmbc.gitlab.io/2020

July 19, 2020

Co-located with the 32nd International Conference on Computer-Aided 
Verification (CAV 2020)


http://i-cav.org/2020/

*Due do the COVID-19 pandemic, the workshop is likely to be held online.*

-
IMPORTANT DATES

Abstract submission: May 12, 2020 (extended)
Full paper submission: May 19, 2020 (extended)
Notification: June 23, 2020 (extended)
Camera-ready: July 14, 2020 (extended)
Conference: July 19, 2020

Deadlines are Anywhere on Earth:
https://en.wikipedia.org/wiki/Anywhere_on_Earth



TOPICS OF INTEREST


Blockchains are decentralized transactional ledgers that rely on
cryptographic hash functions for guaranteeing the integrity of the
stored data. Participants on the network reach agreement on what valid
transactions are through consensus algorithms.

Blockchains may also provide support for Smart Contracts. Smart
Contracts are scripts of an ad-hoc programming language that are
stored in the Blockchain and that run on the network. They can
interact with the ledger’s data and update its state. These scripts
can express the logic of possibly complex contracts between users of
the Blockchain. Thus, Smart Contracts can facilitate the economic
activity of Blockchain participants.

With the emergence and increasing popularity of cryptocurrencies such
as Bitcoin and Ethereum, it is now of utmost importance to have strong
guarantees of the behavior of Blockchain software.
These guarantees can be brought by using Formal Methods. Indeed,
Blockchain software encompasses many topics of computer science where
using Formal Methods techniques and tools are relevant: consensus
algorithms to ensure the liveness and the security of the data on the
chain, programming languages specifically designed to write Smart
Contracts, cryptographic protocols, such as zero-knowledge proofs,
used to ensure privacy, etc.

This workshop is a forum to identify theoretical and practical
approaches of formal methods for Blockchain technology. Topics
include, but are not limited to:
* Formal models of Blockchain applications or concepts
* Formal methods for consensus protocols
* Formal methods for Blockchain-specific cryptographic primitives or 
protocols

* Design and implementation of Smart Contract languages
* Verification of Smart Contracts



SUBMISSION


Submit original manuscripts (not published or considered elsewhere)
with a maximum of twelve pages (full papers), six pages (short
papers), and two pages (extended abstract) describing new and emerging
ideas or summarizing existing work). Each paper should include a title
and the name and affiliation of each author. Authors of selected
extended-abstracts are invited to give a short lightning talk.

At least one author of an accepted paper is expected to present the
paper at the workshop as a registered participant.

Submission link: https://easychair.org/conferences/?conf=fmbc2020

The authors are encouraged to use LaTeX and the EasyChair style files:
https://easychair.org/publications/for_authors



PROCEEDINGS


All submissions will be peer-reviewed by at least three members of the
program committee for quality and relevance. Accepted regular papers
(full and short papers) will be included in the workshop proceedings,
published as a volume of the OpenAccess Series in Informatics (OASIcs)
by Dagstuhl.



INVITED SPEAKER


Grigore Rosu, Professor at University of Illinois at Urbana-Champaign,
USA and Founder of Runtime Verification

http://fsl.cs.illinois.edu/index.php/Grigore_Rosu
https://runtimeverification.com/



PROGRAM COMMITTEE


PC CO-CHAIRS
* Bruno Bernardo (Nomadic Labs, France) (br...@nomadic-labs.com)
* Diego Marmsoler (University of Exeter, UK) (d.marmso...@exeter.ac.uk)

PC MEMBERS
* Wolfgang Ahrendt (Chalmers University of Technology, Sweden)
* Lacramioara Astefanoei (Nomadic Labs, France)
* Massimo Bartoletti (University of Cagliari, Italy)
* Bernhard Beckert (Karlsruhe Institute of Technology, Germany)
* Achim Brucker (University of Exeter, UK)
* Silvia Crafa (Universita di Padova, Italy)
* Zaynah Dargaye (Nomadic Labs, France)
* Jérémie Decouchant 

[TYPES/announce] 3rd CfP: 13th Interaction and Concurrency Experience (ICE 2020)

[Alceste Scalas]

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

CALL FOR ORAL COMMUNICATIONS AND SHORT PAPERS

   ICE 2020
 13th Interaction and Concurrency Experience
 19 June 2020
 Satellite workshop of DisCoTec 2020

   http://www.discotec.org/2020/ice

   Submission link:
https://openreview.net/group?id=DisCoTec.org/2020/Workshop/ICE


=== HIGHLIGHTS ===

* Distinctive selection procedure
* ICE welcomes oral communications of already published or
  preliminary work
* Deadlines: 8 May (abstract submission), 11 May (paper submission)

* Invited speakers:
  - Cinzia Di Giusto (Université Côte d’Azur, CNRS, I3S, France)
  - Karoliina Lehtinen (University of Liverpool, UK)


=== COVID-19 UPDATE ===

Due to the ongoing COVID-19 outbreak, ICE 2020 will be held online, as
the rest of DisCoTec. No physical meeting/presentations will take
place. Instead, the authors of accepted papers will give their talks
remotely (or record their talks if they prefer), and discuss with the
conference participants online. More details will follow.


=== IMPORTANT DATES (UPDATED) ===

* Oral communications and short papers:
* 8 May 2020: abstract submission
* 11 May 2020: paper submission

* 4 June 2020: notification
* 19-20 June 2020: ICE workshop


=== SCOPE ===

Interaction and Concurrency Experience (ICE) is a series of
international scientific meetings oriented to theoretical computer
science researchers with special interest in models, verification,
tools, and programming primitives for complex interactions.

The general scope of the venue includes theoretical and applied
aspects of interactions and the synchronization mechanisms used among
components of concurrent/distributed systems, related to several areas
of computer science in the broad spectrum ranging from formal
specification and analysis to studies inspired by emerging
computational models.

We solicit contributions relevant to Interaction and Concurrency,
including but not limited to:

* Formal semantics
* Process algebras and calculi
* Models and languages
* Protocols
* Logics and types
* Expressiveness
* Model transformations
* Tools, implementations, and experiments
* Specification and verification
* Coinductive techniques
* Tools and techniques for automation
* Synthesis techniques


=== SELECTION PROCEDURE ===

Since its first edition in 2008, the distinguishing feature of ICE has
been an innovative paper selection mechanism based on an interactive,
friendly, and constructive discussion amongst authors and PC members
in an online forum.

During the review phase, each submission is published in a dedicated
discussion forum. The discussion forum can be accessed by the authors
of the submission and by all PC members not in conflict with the
submission (the forum preserves anonymity). The forum is used by
reviewers to ask questions, clarifications, and modifications from the
authors, allowing them better to explain and to improve all aspects of
their submission. The evaluation of the submission will take into
account not only the reviews, but also the outcome of the discussion.

As witnessed by the past nine editions of ICE, this procedure
considerably improves the accuracy of the reviews, the fairness of the
selection, the quality of camera-ready papers, and the discussion
during the workshop.

ICE adopts a light double-blind reviewing process, detailed below.


=== SUBMISSION GUIDELINES ===

Submissions must be made electronically in PDF format via OpenReview:

https://openreview.net/group?id=DisCoTec.org/2020/Workshop/ICE

We invite two types of submissions:

* Research papers, original contributions that will be published
  in the workshop post-proceedings. NOTE: the deadline for
  research papers has passed

* Oral communications will be presented at the workshop, but will
  not appear in the post-proceedings. This type of contribution
  includes e.g. previously published contributions, preliminary
  work, and position papers. There is no strict page limit for
  this kind of submission but papers of 1-5 pages would be
  appreciated. For example, a one page summary of previously
  published work is welcome in this category.

Papers in the “Oral communications” category need not be
anonymized. For any questions concerning the double blind process,
feel free to consult the ICEcreamers.

We are keen to enhance the balanced, inclusive and diverse nature of
the ICE community, and would particularly encourage female colleagues
and members of other underrepresented groups to submit their work.


=== ICECREAMERS ===

Julien Lange (University of Kent, UK) - j.s.la...@kent.ac.uk
Anastasia Mavridou (NASA Ames, USA) -