[TYPES/announce] Principles of Secure Compilation (PriSC) 2020: Call for Participation and Short Talks

2019-12-10 Thread Dominique DEVRIESE
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Principles of Secure Compilation Workshop (PriSC 2020)

  - POPL/PriSC Early registration deadline: 18 December 2019
  - Registration, visa info, venue: https://popl20.sigplan.org/
  - Accepted talks available here:
https://popl20.sigplan.org/home/prisc-2020#event-overview
  - Invited speaker:
Tyler McMullen (Fastly)
  - Call for short talks: see below
Deadline: 13 January 2020

The Workshop on Principles of Secure Compilation (PriSC) is an informal 1-day
workshop without formal proceedings. The goal is to bring together researchers
interested in secure compilation and to identify interesting research directions
and open challenges.

PriSC 2020 will be held on Saturday 25 January 2020 in New Orleans, Louisiana,
United States and will be co-located with POPL 2020.

For more information about this edition and the PriSC series, please
visit https://popl20.sigplan.org/home/prisc-2020

### Invited Speakers

Tyler McMullen (Fastly)

### Accepted papers

The list of accepted talks is available at

https://popl20.sigplan.org/home/prisc-2020#event-overview

### Call for Short Talks

We also have a short talks session, where participants get 5 minutes to present
intriguing ideas, advertise ongoing work, etc. If you're interested in giving a
short 5-minute talk should submit an abstract. Any topic that could be of
interest to the emerging secure compilation community is in scope. Presentations
that provide a useful outside view or challenge the community are also welcome.

  - Deadline: 13 January 2020
  - More details:
https://popl20.sigplan.org/home/prisc-2020#Call-for-Short-Talks
  - Submit here:
https://prisc2020short.hotcrp.com/

### Workshop summary

The emerging field of secure compilation aims to preserve security properties of
programs when they have been compiled to low-level languages such as assembly,
where high-level abstractions don’t exist, and unsafe, unexpected interactions
with libraries, other programs, the operating system and even the hardware are
possible. For unsafe source languages like C, secure compilation requires
careful handling of undefined source-language behavior (like buffer overflows
and double frees). Formally, secure compilation aims to protect high-level
language abstractions in compiled code, even against adversarial low-level
contexts, thus enabling sound reasoning about security in the source language. A
complementary goal is to keep the compiled code efficient, often leveraging new
hardware security features and advances in compiler design. Other necessary
components are identifying and formalizing properties that secure compilers must
possess, devising efficient security mechanisms (both software and hardware),
and developing effective verification and proof techniques. Research in the
field thus puts together advances in compiler design, programming languages,
systems security, verification, and computer architecture.

### Contact

For any questions please contact the workshop chairs, Dominique Devriese
(dominique.devri...@vub.be) and Deian Stefan (de...@cs.ucsd.edu).

To make sure you receive PriSC announcements in the future please
subscribe to the following low-traffic mailing list:
https://lists.gforge.inria.fr/mailman/listinfo/prisc-announce


[TYPES/announce] Lecturer/Senior Lecturer/Reader in Programming Languages for Trustworthy Systems in Edinburgh LFCS

2019-12-10 Thread Philip Wadler
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Lecturer/Senior Lecturer/Reader in Programming Languages for Trustworthy
Systems in Edinburgh LFCS

https://www.vacancies.ed.ac.uk/pls/corehrrecruit/erq_jobspec_version_4.jobspec?p_id=050700

The University of Edinburgh seeks to appoint a Lecturer/Senior
Lecturer/Reader in Programming Languages for Trustworthy Systems.  An ideal
candidate will be able to contribute and complement the expertise of the
Programming Languages & Foundations Group which is part of the Laboratory
for Foundations of Computer Science (LFCS).

The successful candidate will have a PhD, an established research agenda
and the enthusiasm and ability to undertake original research, to lead a
research group, and to engage with teaching and academic supervision, with
expertise in at least one of the following:

   -

   Practical systems verification: e.g. for operating systems, databases,
   compilers, distributed systems
   -

   Language-based verification: static analysis, verified systems / smart
   contract programming, types, SAT/SMT solving
   -

   Engineering trustworthy software: automated/property-based testing, bug
   finding, dynamic instrumentation, runtime verification

We are seeking current and future leaders in the field.

Applications from individuals from underrepresented groups in Computer
Science are encouraged.

Appointment will be full-time and open-ended.

The post is situated in the Laboratory for Foundations of Computer Science,
the Institute in which the School's expertise in functional programming,
logic and semantics, and theoretical computer science is concentrated.
Collaboration relating to PL across the School is encouraged and supported
by the School's Programming Languages Research Programme, to which the
successful applicant will be encouraged to contribute. Applicants whose
PL-related research aligns well with particular strengths of the School,
such as machine learning, AI, robotics, compilers, systems, and security,
are encouraged to apply and highlight these areas of alignment.

All applications must contain the following supporting documents:

• Teaching statement outlining teaching philosophy, interests and plans

• Research statement outlining the candidate’s research vision and future
plans

• Full CV (resume) and publication list

The University job posting and submission site, including detailed
application instructions, is at this link:

https://www.vacancies.ed.ac.uk/pls/corehrrecruit/erq_jobspec_version_4.jobspec?p_id=050700

Applications close at 5pm GMT on January 31, 2020. This deadline is firm,
so applicants are exhorted to begin their applications in advance.

Shortlisting for this post is due early February with interview dates for
this post expected to fall in early April 2020. Feedback will only be
provided to interviewed candidates. References will be sought for all
shortlisted candidates. Please indicate on your application form if you are
happy for your referees to be contacted.

Informal enquiries may be addressed to Prof Philip Wadler (
wad...@inf.ed.ac.uk).

Lecturer Grade: UE08 (£41,526 - £49,553)

Senior Lecturer or Reader Grade: UE09 (£52,559 - £59,135)

The School is advertising a number of positions, including this one, as
described here:

https://www.ed.ac.uk/informatics/about/work-with-us/vacancies/academic-recruitment

About the Laboratory for Foundations of Computer Science

As one of the largest Institutes in the School of Informatics, and one of
the largest theory research groups in the world, the Laboratory for
Foundations of Computer Science combines expertise in all aspects of
theoretical computer science, including algorithms and complexity,
cryptography, database theory, logic and semantics, and quantum computing.
The Programming Languages and Foundations group includes over 25 students,
researchers and academic staff, working on functional programming, types,
verification, semantics, software engineering, language-based security and
new programming models. Past contributions to programming languages
research originating at LFCS include Standard ML, the Edinburgh Logical
Framework, models of concurrency such as the pi-calculus, and foundational
semantic models of effects in programming languages, based on monads and
more recently algebraic effects and handlers.

About the School of Informatics and University of Edinburgh

The School of Informatics at the University of Edinburgh is one of the
largest in Europe, with more than 120 academic staff and a total of over
500 post-doctoral researchers, research students and support staff.
Informatics at Edinburgh rated highest on Research Power in the most recent
Research Excellence Framework. The School has strong links with industry,
with dedicated business incubator space and well-established enterprise and
business development programmes. The School of Informatics has recently
established the Bayes Centre for 

[TYPES/announce] MSFP 2020 - Second Call for Papers

2019-12-10 Thread Sam Lindley

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

Eighth Workshop on
MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING
Saturday 25th April 2020, Dublin, Ireland
A satellite workshop of ETAPS 2020

https://msfp-workshop.github.io/msfp2020/

  ** Deadline: 9th January (abstract), 16th January (paper) **

The eighth workshop on Mathematically Structured Functional
Programming is devoted to the derivation of functionality from
structure. It is a celebration of the direct impact of Theoretical
Computer Science on programs as we write them today. Modern
programming languages, and in particular functional languages, support
the direct expression of mathematical structures, equipping
programmers with tools of remarkable power and abstraction. Where
would Haskell be without monads? Functional reactive programming
without temporal logic?  Call-by-push-value without adjunctions? The
list goes on. This workshop is a forum for researchers who seek to
reflect mathematical phenomena in data and control.

The first MSFP workshop was held in Kuressaare, Estonia, in July 2006,
affiliated with MPC 2006 and AMAST 2006. The second MSFP workshop was
held in Reykjavik, Iceland as part of ICALP 2008. The third MSFP
workshop was held in Baltimore, USA, as part of ICFP 2010. The fourth
workshop was held in Tallinn, Estonia, as part of ETAPS 2012. The
fifth workshop was held in Grenoble, France, as part of ETAPS
2014. The sixth MSFP Workshop was held in April 2016, in Eindhoven,
Netherlands, as part of ETAPS 2016. The seventh MSFP Workshop was held
in July 2018, in Oxford, UK, as part of FLoC 2018.

Important Dates:


Abstract deadline:  9th January  (Thursday)
Paper deadline:16th January  (Thursday)
Notification:  27th February (Thursday)
Final version: 26th March(Thursday)
Workshop:  25th April(Saturday)

Invited Speakers:
=

Pierre-Marie Pédrot - Inria Rennes-Bretagne-Atlantique, France
Satnam Singh- Google Research, USA

Program Committee:
==

Stephanie Balzer  - CMU, USA
Kwanghoon Choi- Chonnam, South Korea
Ralf Hinze- Kaiserslautern, Germany
Marie Kerjean - Inria Nantes, France
Sam Lindley   - Edinburgh and Imperial, UK (co-chair)
Max New   - Northeastern, USA (co-chair)
Fredrik Nordvall-Forsberg - Strathclyde, UK
Alberto Pardo - Montevideo, Uruguay
Exequiel Rivas Gadda  - Inria Paris, France
Claudio Russo - DFINITY, UK
Tarmo Uustalu - Reykjavik, Iceland
Nicolas Wu- Imperial, UK
Maaike Zwart  - Oxford, UK

Submission:
===

Submissions are welcomed on, but by no means restricted to, topics
such as:

structured effectful computation
structured recursion
structured corecursion
structured tree and graph operations
structured syntax with variable binding
structured datatype-genericity
structured search
structured representations of functions
structured quantum computation
structure directed optimizations
structured types
structure derived from programs and data

Please contact the programme chairs Sam Lindley (sam.lind...@ed.ac.uk)
and Max New (max...@ccs.neu.edu) if you have any questions about the
scope of the workshop.

We accept two categories of submission: full papers of no more than 15
pages that will appear in the proceedings, and extended abstracts of
no more than 2 pages that we will post on the website, but which do
not constitute formal publications and will not appear in the
proceedings. References and appendices are not included in page
limits. Appendices may not be read by reviewers.

Submissions must report previously unpublished work and not be
submitted concurrently to another conference with refereed
proceedings. Accepted papers must be presented at the workshop by one
of the authors. The proceedings will be published under the auspices
of EPTCS with a Creative Commons license.

A short abstract should be submitted a week in advance of the paper
deadline (for both full paper and extended abstract submissions).

We are using EasyChair to manage submissions. To submit a paper, use
this link:

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

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.



[TYPES/announce] CfP: ProvenanceWeek, IPAW, and TaPP 2020

2019-12-10 Thread James Cheney
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


Call for Papers
   4th ProvenanceWeek
8th International Provenance and Annotation Workshop (IPAW '20)
12th USENIX Workshop on the Theory and Practice of Provenance (TaPP '20)
  ---
  June 22-25, 2020, UNC Charlotte, USA
  ---
https://provenanceweek.org/2020/



=
OVERVIEW
=

Provenance describes the entities and processes involved in producing or
otherwise influencing a resource. It provides a critical foundation for
assessing the authenticity of computationally derived results, enabling
trust,
and facilitating reuse and reproducibility. Provenance provides insight
into the
origins and derivation of data for data quality assessments, debugging and
search.

Topics in provenance include capture, storage, usage, security,
interoperability, and applications. Of particular interest are the
fundamental
problems that must be solved in order to make provenance a useful and usable
tool in the world today: What theoretical problems need to be solved? What
practical problems can we tackle? What lessons have we learned from real
implementations?

Continuing the first three successful ProvenanceWeek events in 2014, 2016,
and
2018, ProvenanceWeek 2020 aims to provide a venue for both mature research
contributions and early-stage research in the area of provenance, and to
attract
a broad audience of researchers working on provenance techniques,
researchers in
other disciplines that make use of, or apply, provenance techniques, and
participants from industry or government.

ProvenanceWeek 2020 will feature two primary events organized into tracks,
the
International Provence and Annotation Workshop (IPAW) track and the Theory
and
Practice of Provenance (TaPP) track, and in addition, will feature a joint
poster/demo track.

==
Topics
==

The goal of ProvenanceWeek is to bring together researchers and
practitioners
who are studying, applying, and advancing provenance in scientific and
scholarly
uses.

Topics of interest for ProvenanceWeek include, but are not limited to the
following:

* Provenance visualization, and human interaction with provenance
* Provenance for big data and extreme computing
* Provenance for attribution and trust
* Provenance for transparency and accountability
* Security and privacy implications of provenance
* Provenance, social media, and the semantic web
* Provenance analytics, discovery, and reasoning about provenance and its
quality
* Data sharing and data citation
* Provenance of workflows and annotations
* Standardization of provenance models, services, and representations
* Provenance management system prototypes and commercial solutions
* Applications of provenance in real-life settings
* Theoretical foundations of provenance
* Connections between provenance and established topics in other research
fields
  (programming languages, security, software engineering, fairness, etc.)
* Provenance-based audit and forensics
* Design, performance and scalability of provenance systems

===
Important Dates
===

- Co-located event proposal deadline:   February 1, 2020
- Co-located event acceptance notification: February 15, 2020
- Abstract deadline:March 1, 2020
- Paper deadline:   March 8, 2020
- Demo / Poster deadline:   April 9, 2020
- Author notification:  May 1, 2020
- Camera ready due: June 4, 2020

=
Conference Organizers
=

- Boris Glavic (Illinois Institute of Technology, USA) - ProvenanceWeek PC
Chair
- Vanessa Braganholo (Universidade Federal Fluminense, Brazil) - IPAW PC
Chair
- Thomas Pasquier (University of Bristol, UK) - TaPP PC Chair
- David Koop (Northern Illinois University, USA) - Poster/Demo Chair
- Thomas Moyer (University of North Carolina at Charlotte, USA) - Local
Chair

===
Submissions
===

Authors can submit papers to either the IPAW, TaPP, or demo/poster track of
ProvenanceWeek. Submission of the same or closely related work to both
tracks is
expressly disallowed. The submission site for all tracks is:

https://pw2020.thomasmoyer.org/pw2020/

==
IPAW Track Research Papers
==

Authors are invited to submit original research work the IPAW track. This
track
solicits full research papers that describe mature, high-quality research
on the
topics of interest of the Provenance Week. Papers 

[TYPES/announce] BCTCS & AlgoUK 2020 - Announcement and call for contributed talks

2019-12-10 Thread Berger U.
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Announcement and call for contributed talks:
BCTCS & AlgoUK 2020
BRITISH COLLOQUIUM FOR THEORETICAL COMPUTER SCIENCE
6th - 8th April 2020, SWANSEA

http://www.cs.swan.ac.uk/bctcs2020

The 36th British Colloquium for Theoretical Computer Science will take
place in Swansea from the afternoon of Monday 6 April to Wednesday 8
April 2020.

The purpose of BCTCS is to provide a forum in which researchers in
theoretical computer science can meet, present research findings, and
discuss developments in the field. It also aims to provide an
environment in which PhD students can gain experience in presenting
their work, and benefit from contact with established researchers.

The scope of the colloquium includes all aspects of theoretical computer
science, including automata theory, algorithms, complexity theory,
semantics, formal methods, concurrency, game theory, types, languages
and logics.

BCTCS 2020 is being held together with the Fourth AlgoUK workshop which
includes a session on Verification of Railway Control Systems. There
will also be a special evening public forum on Formal Methods in
Software Engineering.

The list of Invited Speakers includes

  Petra Berenbrink - University of Hamburg (TBC)
  Simon Chadwick - Siemens Rail Automation UK (TBC)
  Robert Constable - Cornell University
  Mike Hinchley - University of Limerick
  Cliff Jones - University of Newcastle
  Bas Luttik - University of Eindhoven
  Tom Maibaum - McMaster University
  David Manlove - University of Glasgow
  Jan Peleska - Bremen University
  Patrick Totzke - University of Liverpool
  Helen Treharne - University of Surrey
  John Tucker - Swansea University (TBC)
  Kristina Vuskovic - University of Leeds

SUBMISSION OF PRESENTATIONS

Participants wishing to give a 30 minute contributed talk on any topic
within the scope of the colloquium are invited to submit a title and
abstract via the BCTCS'2020 webpage. Presentations from research
students and early career researchers are particularly encouraged. The
titles and abstracts of all invited and contributed talks will appear in
the Bulletin of the EATCS.

REGISTRATION AND BURSARIES

Registration information is available at the BCTCS'2020 webpage.

We have a number of bursaries worth £200 which can be used to reimburse
the travel and accommodation expenses of UK-based researchers and PhD
students. We hope to be able to offer these to all participants who
provide a talk; but in the case of over-subscription, they will be
allocated on a first-come, first-served basis. Hence, do propose a talk
early.

IMPORTANT DATES (DEADLINES)

  Talk proposals: 1 February 2020
  Registration: 1 March 2020
  Meeting: 6-8 April 2020

SPONSORS

  London Mathematical Society
  Heilbronn Institute for Mathematical Research
  BCTCS
  AlgoUK
  Institute of Coding in Wales
  Technocamps

---

BCTCS & AlgoUK 2020 Organizing Committee:
Ulrich Berger, Phil James, Faron Moller, Liam O'Reilly, Filipos
Pantekis, Olga Petrovska, Markus Roggenbach, Monika Seisenberger
(Swansea University);
and Daniel Paulusma, Iain Stewart (Durham University)



[TYPES/announce] PhD candidate or Postdoc position (Uni Amsterdam) in programming languages for multi-core embedded systems

2019-12-10 Thread Clemens Grelck
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The _Parallel Computing Systems (PCS)_ group at the Informatics 
Institute (IvI)  of the University of Amsterdam 
(UvA)  is looking for a PhD candidate or a 
postdoctoral researcher (depending on prior qualification) to work 
within the EU-funded Horizon-2020 project ADMORPH. The ADMORPH 
consortium brings together 4 academic and 4 industrial partners from 
across Europe and is coordinated by the University of Amsterdam.


The successful candidate will conduct research in the area of 
domain-specific programming languages, including their compilers and 
runtime systems, for heterogeneous multi-core adaptive cyber-physical 
systems that are robust against component failure and cyber-attacks. 
Further details as well as instructions for application can be found at 
our official vacancies site:

https://www.uva.nl/en/content/vacancies/2019/10/19-725-researcher-in-specification-and-programming-of-adaptive-cyber-physical-systems.html

Closing date: December 12, 2019.

For informal inquiries, please contact:
 Dr Clemens Grelck .

--
--
Dr Clemens Grelck Science Park 904
Associate Professor   1098XH Amsterdam
Programme Director Software EngineeringNetherlands

University of Amsterdam
Institute for InformaticsT +31 (0) 20 525 8683
System and Network Engineering Lab   F +31 (0) 20 525 7490

Office C3.109 staff.fnwi.uva.nl/c.u.grelck
--



[TYPES/announce] Reversible Computation 2020 CfP

2019-12-10 Thread ivan.lanese
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


We apologize if you receive multiple copies of this Call for Papers.
Please distribute to anyone who may be interested.
===

12th Conference on Reversible Computation
(RC 2020)

July 9th-10th, 2020, Oslo, Norway
Abstract Submission: January 31th, 2020
Submission Deadline: February 7th, 2020
https://reversible-computation-2020.github.io/

===

Reversible computation has a growing number of promising application areas 
such as low power design, coding/decoding, debugging, testing and 
verification, database recovery, discrete event simulation, reversible 
algorithms, reversible specification formalisms, reversible programming 
languages, process algebras, and the modeling of biochemical systems. 
Furthermore, reversible logic provides a basis for quantum computation 
with its applications, for example, in cryptography and in the development 
of highly efficient algorithms. First reversible circuits and quantum 
circuits have been implemented and are seen as promising alternatives to 
conventional CMOS technology.


The conference will bring together researchers from computer science, 
mathematics, and physics to discuss new developments and directions for 
future research in Reversible Computation. This includes applications of 
reversibility in quantum computation. Research papers, tutorials, tool 
demonstrations, and work-in-progress reports are within the scope of the 
conference. Invited talks by leading international experts will complete 
the program. Contributions on all areas of Reversible Computation are 
welcome, including---but not limited to---the following topics:


* Applications
* Architectures
* Algorithms
* Bidirectional transformations
* Circuit Design
* Debugging
* Fault Tolerance and Error Correction
* Hardware
* Information Theory
* Physical Realizations
* Programming Languages
* Quantum Computation
* Software
* Synthesis
* Theoretical Results
* Testing
* Verification

= Important Dates =

Abstract submission: January 31, 2020
Submission deadline: February 7, 2020
Notification to authors: March 20, 2020
Final version:   April 10, 2020
Conference:  July 9 - July 10, 2020

= Invited speakers =

TO BE ANNOUNCED

= Paper submission =

Interested researchers are invited to submit full research papers (16
pages maximum), tutorials (16 pages maximum), as well as
work-in-progress or tool demonstration papers (6 pages maximum) in
Springer LNCS format.  Additional material intended for reviewers but
not for publication in the final version - for example, details of
proofs - may be placed in a clearly marked appendix that is not
included in the page limit. Reviewers are at liberty to ignore
appendices and papers must be understandable without them.
Contributions must be written in English and report on original,
unpublished work, not submitted for publication elsewhere. Submissions
not adhering to the specified constraints may be rejected without
review. Each paper will undergo a peer review of at least 3 anonymous
reviewers. All accepted papers will be included in the conference
proceedings and published by Springer as a Lecture Notes in Computer
Science (LNCS) volume. Papers can be submitted electronically in pdf
via the RC 2020 interface of the EasyChair system:

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

= General Chair =

Rudolf Schlatte
University of Oslo
Norway

= Program Chairs =

Ivan Lanese
University of Bologna/INRIA
Italy

Mariusz Rawski
Warsaw University of Technology
Poland

= Program Committee =

 * Gerhard Dueck (University of New Brunswick, Canada)
 * Robert Glück (University of Copenhagen, Denmark)
 * Jarkko Kari (University of Turku, Finland)
 * Jean Krivine (CNRS, France)
 * Martin Lukac (Nazarbayev University, Kazakhstan)
 * Kazutaka Matsuda (Tohoku University, Japan)
 * Claudio Antares Mezzina (Università di Urbino, Italy)
 * Lukasz Mikulski (Nicolaus Copernicus University, Poland)
 * Torben Ægidius Mogensen (University of Copenhagen, Denmark)
 * Claudio Moraga (TU Dortmund University, Germany)
 * Iain Phillips (Imperial College London, UK)
 * Krzysztof Podlaski (University Of Lodz, Poland)
 * Markus Schordan (Lawrence Livermore National Laboratory, US)
 * Peter Selinger (Dalhousie University, Canada)
 * Mathias Soeken (Ecole Polytechnique Fédérale de Lausanne, Switzerland)
 * Milena Stankovic (University of Nis, Serbia)
 * Himanshu Thapliyal (University of Kentucky, US)
 * Irek Ulidowski (University of Leicester, UK)
 * German Vidal (Universitat Politecnica de Valencia, Spain)
 * Robert Wille (Johannes Kepler University Linz, Austria)
 * Tetsuo Yokoyama (Nanzan University, Japan)

= Contacts =

rc2...@easychair.org