[TYPES/announce] Postdoc positions in CertiChain project

[Sergey, Ilya]

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

Greetings all,

I have several postdoc positions available in my group at School of Computing 
of National University of Singapore in the new project CertiChain, funded by 
NSOE-TSS. The positions are initially for two years with a possibility of 
extension.

The CertiChain project focuses on mechanising safety, liveness, and 
probabilistic security properties of distributed protocols, with a specific 
focus on Nakamoto-style consensus. I am looking for motivated candidates with a 
strong, internationally competitive research track record and research 
expertise in:
- distributed systems and consensus protocols
- formal verification using program logics
- mechanised proofs and proof automation

More details on the project can be found by the link below:

  https://certichain.github.io

The NUS School of Computing is one of the world-leading departments in the 
areas of programming languages, software engineering, distributed systems, 
security and privacy. It provides a diverse and welcoming environment. Salaries 
at NUS are internationally competitive.

Do not hesitate to get in touch with me if you are interested.

Kind regards,
Ilya



Important: This email is confidential and may be privileged. If you are not the 
intended recipient, please delete it and notify us immediately; you should not 
copy or use it for any purpose, nor disclose its contents to any other person. 
Thank you.

[TYPES/announce] Postdoc position at National University of Singapore on Program Synthesis

[Sergey, Ilya]

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

Hello all,

I invite candidates for a postdoc position, which is available in my group at 
Yale-NUS College and School of Computing of National University of Singapore. 
The position is for two years, funded by Singapore MOE Tier 1 grant "Scalable 
Deductive Synthesis of Thread-Safe Concurrency".

As the project name implies, we will be working on synthesising 
correct-by-construction concurrent programs. I am looking for motivated 
candidates with a strong, internationally competitive research track record. 
Particularly relevant is research expertise in:
- formal verification using program logics
- concurrent programming and concurrent data structures
- SMT and decision procedures

A tentative starting date is 1 October 2019, but the appointment can start 
earlier if the position is filled. The successful candidate is expected to work 
with me and external collaborators (specifically, Prof. Nadia Polikarpova from 
UC San Diego), as well as to help advising students and interns on the project 
topic, but can also allocate some part of their time for the projects of their 
interest.

The NUS School of Computing is one of the world-leading departments in the 
areas of programming languages, software engineering, distributed systems, 
security and privacy. It provides a diverse and welcoming environment, and the 
researchers from different groups at SoC frequently collaborate on joint 
projects of mutual interest.

Official advert: https://www.yale-nus.edu.sg/careers/postdoctoral-fellow-2/

Do not hesitate to get in touch with me if you are interested!

Kind regards,
Ilya




Important: This email is confidential and may be privileged. If you are not the 
intended recipient, please delete it and notify us immediately; you should not 
copy or use it for any purpose, nor disclose its contents to any other person. 
Thank you.

[TYPES/announce] CoqPL'18: call for participations and final programme

[Sergey, Ilya]

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

=
 CoqPL 2018

 Coq for Programming Languages
 --
   A Coq users and developers meeting
   13 January 2018, co-located with POPL (as usual)
 Los Angeles, California, United States

  CALL FOR PARTICIPATIONS

  https://popl18.sigplan.org/track/CoqPL-2018
=

Workshop Overview
-

The series of CoqPL workshops provide 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 favourite proof assistant.

The exciting final progamme is now available at:
https://popl18.sigplan.org/track/CoqPL-2018#program

Workshop Programme
--

9:00-10:00: Keynote
* CoqHammer: Strong Automation for Program Verification
  Łukasz Czajka and Cezary Kaliszyk
10:30-12:10: Tactics and Proof Engineering
* A “destruct” Tactic for Mtac2
  Jan-Oliver Kaiser and Beta Ziliani
* Typed Template Coq
  Simon Boulier, Matthieu Sozeau, Nicolas Tabareau and Abhishek Anand
* Elpi: an extension language for Coq
  Enrico Tassi
* Coqatoo: Generating Natural Language Versions of Coq Proofs
  Andrew Bedford
14:00-14:50: PL Metatheory
* Locally Nameless at Scale
  Stephanie Weirich, Antoine Voizard and Anastasiya Kravchuk-Kirilyuk
* A Coq Formalisation of a Core of R
  Martin Bodin

14:50-15:30: Coq Deveveloprs Talk & Panel
16:00-18:05: Semantics and Synthesis
* Revisiting Parametricity: Inductives and Uniformity of Propositions
  Abhishek Anand and Greg Morrisett
* Phantom Types for Quantum Programs
  Robert Rand, Jennifer Paykin and Steve Zdancewic
* Towards Context-Aware Data Refinement
  Paul Krogmeier, Steven Kidd and Benjamin Delaware
* Mechanizing the Construction and Rewriting of Proper Functions in Coq
  Edwin Westbrook
* A calculus for logical refinements in separation logic
  Dan Frumin and Robbert Krebbers

Contact
-

For any queries, please contact : coqpl2018 at 
easychair.org

Kind regards,
Yves Bertot and Ilya Sergey

[TYPES/announce] CoqPL'18 CFP: Deadline Extended till 20 October

[Sergey, Ilya]

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

=
 CoqPL 2018

 Coq for Programming Languages
 --
   A Coq users and developers meeting
   13 January 2018, co-located with POPL (as usual)
 Los Angeles, California, United States

 CALL FOR PRESENTATIONS

  https://popl18.sigplan.org/track/CoqPL-2018
=


Workshop Overview
-

The series of CoqPL workshops provide 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 favourite proof assistant.

Topics in scope include but are no limited to:

* General purpose libraries and tactic language extensions;

* Domain-specific libraries for programming language formalization and
  verification;

* IDEs, profilers, tracers, debuggers, and testing tools;

* Reports on ongoing proof efforts conducted via (or in the context
  of) the Coq proof assistant;

* 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.


Workshop Format
---

The workshop format will be driven by members of the Coq 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. Talks will be selected according to relevance to the workshop,
based on the submission of an extended abstract.


Submission Details
--

* Abstract Submission : [extended!] October 20th, 2017
* Author Notification : Monday, November 6th, 2017
* Workshop: Saturday, January 13th, 2018

Submissions should be extended abstracts of 1-2 pages in portable
document format (PDF). Submission is via EasyChair:

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

Program Committee
-

* Yves Bertot, INRIA (Workshop Co-chair)
* Ilya Sergey, University College London (Workshop Co-chair)

* Andrew Appel, Princeton University
* Benjamin Delaware, Purdue University
* Xinyu Feng, University of Science and Technology of China
* Hugo Herbelin, INRIA
* Chantal Keller, Université Paris-Sud
* Ekaterina Komendantskaya, Heriot-Watt University
* Beta Ziliani, Universidad Nacional de Córdoba

Contact
-

For any queries, please contact : coqpl2018 at 
easychair.org

[TYPES/announce] CoqPL 2018: Call for Presentations

[Sergey, Ilya]

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



 CoqPL 2018

 Coq for Programming Languages
 --
   A Coq users and developers meeting
   13 January 2018, co-located with POPL (as usual)
 Los Angeles, California, United States

 CALL FOR PRESENTATIONS

   https://popl18.sigplan.org/track/CoqPL-2018



Workshop Overview
-

The series of CoqPL workshops provide 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 favourite proof assistant.

Topics in scope include but are no limited to:

* General purpose libraries and tactic language extensions;

* Domain-specific libraries for programming language formalization and
  verification;

* IDEs, profilers, tracers, debuggers, and testing tools;

* Reports on ongoing proof efforts conducted via (or in the context
  of) the Coq proof assistant;

* 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.


Workshop Format
---

The workshop format will be driven by members of the Coq 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. Talks will be selected according to relevance to the workshop,
based on the submission of an extended abstract.


Submission Details
--

* Abstract Submission : Monday, October, 16th, 2017
* Author Notification : Tuesday, November 6th, 2017
* Workshop: Saturday, January 13rd, 2018

Submissions should be extended abstracts of 1-2 pages in portable
document format (PDF). Submission is via EasyChair:

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

Program Committee
-

* Yves Bertot, INRIA (Workshop Co-chair)
* Ilya Sergey, University College London (Workshop Co-chair)

* Andrew Appel, Princeton University
* Benjamin Delaware, Purdue University
* Xinyu Feng, University of Science and Technology of China
* Hugo Herbelin, INRIA
* Chantal Keller, Université Paris-Sud
* Ekaterina Komendantskaya, Heriot-Watt University
* Beta Ziliani, Universidad Nacional de Córdoba

Contact
-

For any queries, please contact : coqpl2018 at 
easychair.org

[TYPES/announce] ICFP 2017 Student Research Competition: Call for Submissions

[Sergey, Ilya]

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

==
CALL FOR SUBMISSIONS

   SRC at ICFP 2017
Oxford, United Kingdom
 3-9 September 2017

http://icfp17.sigplan.org/track/icfp-2017-Student-Research-Competition

Co-located with the
   International Conference on Functional Programming (ICFP 2017)
==


Student Research Competition


This year ICFP will host a Student Research Competition where
undergraduate and postgraduate students can present posters. The SRC
at the ICFP 2017 consists of three rounds:


* Extended abstract round: All students are encouraged to submit an
extended abstract outlining their research (up to two pages).

* Poster session at ICFP 2017: Based on the abstracts, a panel of
judges will select the most promising entrants to participate in the
poster session which will take place at ICFP. Students who make it to
this round will be eligible for some travel support to attend the
conference. In the poster session, students will have the opportunity
to present their work to the judges, who will select three finalists
in each category (graduate/undergraduate) to advance to the next
round.

* ICFP presentation: The last round will consist of an oral
presentation at the ICFP to compete for the final awards in each
category and selection of an overall winner who will advance to the
ACM SRC Grand Finals.


Prizes
--

* The top three graduate and the top three undergraduate winners will
receive prizes of $500, $300, and $200, respectively.

* All six winners will receive award medals and a two-year
complimentary ACM student membership, including a subscription to
ACM’s Digital Library.

* The names of the winners will be posted on the SRC web site.

* The first place winners of the SRC will be invited to participate in
the ACM SRC Grand Finals, an on-line round of competitions among the
winners of other conference-hosted SRCs.

* Grand Finalists and their advisors will be invited to the Annual ACM
Awards Banquet for an all-expenses-paid trip, where they will be
recognized for their accomplishments along with other prestigious ACM
award winners, including the winner of the Turing Award (also known as
the Nobel Prize of Computing).

* The top three Grand Finalists will receive an additional $500, $300,
and $200. All Grand Finalists will receive Grand Finalist
certificates.

* The ACM, Microsoft Research, and our industrial partners provide
financial support for students attending the SRC. You can find more
information about this on the ACM website. Eligibility The SRC is open
to both undergraduate (not in a PhD program) and graduate students (in
a PhD program). Upon submission, entrants must be enrolled as a
student at their universities, and are ACM student members.

Eligibility
---

The SRC is open to both undergraduate (not in a PhD programme) and
graduate students (in a PhD programme). Upon submission, entrants must
be enrolled as a student at their universities, and are ACM student
members.

Furthermore, there are some constraints on what kind of work may be
submitted.

Previously published work:

Submissions should consist of original work (not yet accepted for
publication). If the work is a continuation of previously published
work, the submission should focus on the contribution over what has
already been published. We encourage students to see this as an
opportunity to get early feedback and exposure for the work they plan
to submit to the next ICFP or POPL.

Collaborative work:

Students are encouraged to submit work they have been conducting in
collaboration with others, including advisors, internship mentors, or
other students. However, submissions are individual, so they must
focus on the contributions of the student.

Submission Details
--

Each submission should include the student author's name,
institutional affiliation, e-mail address, and postal address;
research advisor's name; ACM student member number; category
(undergraduate or graduate); research title; and an extended abstract
addressing the following:

* Problem and Motivation: Clearly state the problem being addressed
 and explain the reasons for seeking a solution to this problem.

* Background and Related Work: Describe the specialized (but
 pertinent) background necessary to appreciate the work. Include
 references to the literature where appropriate, and briefly explain
 where your work departs from that done by others.

* Approach and Uniqueness: Describe your approach in attacking the
 problem and clearly state how your approach is novel.

* Results and Contributions: Clearly show how the results of your work
 contribute to computer science and