[TYPES/announce] DSLDI 2017: Second Call for Talk Proposals

[Lindsey Kuper]

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

*
SECOND CALL FOR TALK PROPOSALS

DSLDI 2017

Fifth Workshop on
Domain-Specific Language Design and Implementation

October 22, 2017
Vancouver, Canada
Co-located with SPLASH

http://2017.splashcon.org/track/dsldi-2017
https://twitter.com/wsdsldi
*

Deadline for talk proposals: 7th of August, 2017

Well-designed and implemented domain-specific languages (DSLs) can
achieve both usability and performance benefits over general-purpose
programming languages. By raising the level of abstraction and
exploiting domain knowledge, DSLs can make programming more
accessible, increase programmer productivity, and support
domain-specific optimizations.

## Workshop Goal

Domain-Specific Language Design and Implementation (DSLDI) is a
workshop intended to bring together researchers and practitioners
interested in discussing how DSLs should be designed, implemented,
supported by tools, and applied in realistic contexts. The focus of
the workshop is on all aspects of this process, from soliciting domain
knowledge from experts, through the design and implementation of the
language, to evaluating whether and how a DSL is successful. More
generally, we are interested in continuing to build a community that
can drive forward the development of modern DSLs.

## Workshop Format

DSLDI is a single-day workshop and will consist of an invited speaker
followed by moderated audience discussions structured around a series
of short talks. The role of the talks is to facilitate interesting and
substantive discussion. Therefore, we welcome and encourage talks that
express strong opinions, describe open problems, propose new research
directions, and report on early research in progress.

Proposed talks should be on topics within DSLDI’s area of interest,
which include but are not limited to:

  * solicitation and representation of domain knowledge
  * DSL design principles and processes
  * DSL implementation techniques and language workbenches
  * domain-specific optimizations
  * human factors of DSLs
  * tool support for DSL users
  * community and educational support for DSL users
  * applications of DSLs to existing and emerging domains
  * studies of usability, performance, or other benefits of DSLs
  * experience reports of DSLs deployed in practice

## Call for Talk Proposals

We solicit talk proposals in the form of short abstracts (max. 2
pages). A good talk proposal describes an interesting position, open
problem, demonstration, or early achievement. The submissions will be
reviewed on relevance and clarity, and used to plan the mostly
interactive sessions of the workshop day. Publication of accepted
abstracts and slides on the website is voluntary.

* Deadline for talk proposals: August 7th, 2017
* Notification: September 11th, 2017
* Workshop: October 22nd, 2017
* Submission website: https://dsldi17.hotcrp.com/

## Workshop Organization

Co-chairs:

* Lindsey Kuper (lind...@composition.al), Intel Labs
* Eric Walkingshaw (eric.walkings...@oregonstate.edu), Oregon State
University

Follow us on Twitter at https://twitter.com/wsdsldi

Program committee:

* Nada Amin (EPFL/University of Cambridge)
* Eric Holk (Google)
* Gabriele Keller (Data61, CSIRO (formerly NICTA) and UNSW)
* Rebekah Leslie-Hurd (Intel Labs)
* Chris Martens (NCSU)
* Lee Pike (Galois)
* Jonathan Ragan-Kelley (UC Berkeley)
* Jesús Sánchez Cuadrado (Autonomous University of Madrid)
* Vincent St-Amour (Northwestern University)
* Philip Wadler (University of Edinburgh)

[TYPES/announce] DeepSpec summer school is online!

[Benjamin C. Pierce]

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

The DeepSpec Summer School on Verified Systems was held in Philadelphia during 
the last two weeks of July.  If you weren’t able to join in person, you may 
like to know that all the lectures, lecture materials, and exercises are online:

https://deepspec.org/event/dsss17/

Enjoy!

   - Benjamin

[TYPES/announce] Postdoctoral position on effects and/or type theory at Inria in Nantes

[Guillaume Munch-Maccagnoni]

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

Dear all,


We are pleased to announce the availability of a postdoctoral position
on effects and/or type theory in the Inria team Gallinette, in Nantes.

Gallinette is a new Inria team dedicated to the advancement of proof
assistants with an emphasis on mathematical foundations. It is led by
Nicolas Tabareau and hosted by the new Laboratory of Digital Sciences
of Nantes (LS2N). Nantes is a lively and affordable city in Brittany,
not far from the shores of the Atlantic.

We are interested in foundations and applications of proof assistants
and certified programming, especially type theory, the theory of
effects, and their interaction. Relevant topics and experience
include, but is not limited to:

* Homotopy type theory
* Developments in Coq, Agda, Lean, F* or Idris
* Development of (part of) a proof assistant or a programming language
* Semantics of effects and resources
* Rewriting
* Proof theory
* Logical relations and realizability

We are opening a postdoctoral position for 1 year (deadline for
applications: September 15th, job starting between October and March
2018). The successful applicant will join the Inria team Gallinette
and the ERC project CoqHoTT . The
salary and benefits are the standard Inria conditions.

We are looking for excellent researchers with a strong expertise in
one or several relevant topics. Candidates should hold a PhD in
computer science or a closely related field (or be close to complete
their PhD). The new collaborator is expected to participate in the
life of the lab and interact with members of the team including PhD
students and other postdocs.

If you are interested in joining the Gallinette team and have informal
inquiries, please contact either of us at 
or  as soon as possible.
Applications should be sent to either of us by September 15th and must
contain a CV, a research statement, and a list of references.


Sincerely,
Guillaume Munch-Maccagnoni
Nicolas Tabareau

[TYPES/announce] Call for Participation: Workshop on HoTT/UF (with FSCD 2017)

[Anders Mortberg]

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

==
CALL FOR PARTICIPATION
Workshop on Homotopy Type Theory and Univalent Foundations
(HoTT/UF, at FSCD 2017)
September 8-9, 2017, Oxford, United Kingdom
https://hott-uf.github.io/2017/
==

Contents:
1. Invited talks
2. Contributed talks now on the website
3. Post-proceedings with MSCS


1. Invited talks/tutorials
==
* Thorsten Altenkirch (University of Nottingham):
  Naïve Type Theory (tutorial)
* Ulrik Buchholtz (Technical University of Darmstadt):
  Formalizing type theory in type theory using nominal techniques
* Thierry Coquand (University of Gothenburg):
  Sheaf models for univalent type theory

2. Contributed talks

Titles and abstracts for the contributed talks are now available
on the website:
https://hott-uf.github.io/2017/

3. Post-proceedings with MSCS
=
The publication of post-proceedings of the HoTT/UF'17
workshop is being planned, as a special issue of
*Mathematical Structures in Computer Science* (CUP).

Submission to the post-proceedings will be open to all,
with a submission deadline in late spring 2018.
More details will be announced in due course.

[TYPES/announce] Postdoc Position in Program Verification at Carnegie Mellon University, Silicon Valley

[Pasareanu, S Corina (ARC-TI)[SGT, INC]]

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

A post-doctoral researcher position focusing on symbolic verification 
techniques for cyber-security is available at Carnegie Mellon University at the 
Silicon Valley Campus (Mountain View, CA). The research project titled 
"Integrated Symbolic execution for Space-Time Analysis of Code (ISSTAC)" 
involves symbolic execution of Java Bytecode for automatically identifying (1) 
denial of service attacks (by determining worst case complexity of a program in 
terms of both time and space usage) and (2) side channel attacks (by 
determining if observations about the execution time or memory usage of a 
program can leak secret information). This is a multi-year collaborative effort 
with researchers from Vanderbilt University, University of California at Santa 
Barbara and Queen Mary University, London. There are many research directions 
within the scope of this project, including constraint solving and model 
counting techniques, heuristics for scalable symbolic program analysis, 
automated worst-case behavior analysis, quantitative information flow using 
symbolic execution, attack and defense synthesis, distributed computations, 
combinations of symbolic execution and fuzzing, etc.


Candidates for the post-doctoral position should have a doctoral degree in 
computer science (or related field) and should have familiarity with symbolic 
execution techniques and SMT-solvers. Security knowledge is a plus. Candidates 
interested in this position should e-mail a CV, brief statement of research 
interests and a reference (with e-mail address) to Corina Pasareanu 
(corina.pasare...@west.cmu.edu).

The position is available now and will be open until filled. You can find more 
information about the ISSTAC project here 
http://www.cmu.edu/silicon-valley/research/isstac/.

[TYPES/announce] PLAS 2017 - Deadline Extension 4 August 2017

[Nataliia Bielova]

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

PLAS 2017 Call for Papers
ACM SIGSAC 12th Workshop on Programming Languages and Analysis for Security 
(PLAS 2017)

http://plas2017.cse.buffalo.edu/ 

30 October 2017
Dallas, TX, USA

Co-located with ACM CCS 2017 (https://www.sigsac.org/ccs/CCS2017/ 
)

—

Invited Speakers

Stephen Chong, Harvard University, USA
Michael Hicks, University of Maryland, USA

—

Important Dates

Submissions due (EXTENDED): 04 August 2017 (anywhere on Earth)
Author notification:04 September 2017
Final papers due:   17 September 2017
Workshop date:  30 October 2017

—

PLAS aims to provide a forum for exploring and evaluating ideas on the use
of programming language and program analysis techniques to improve the
security of software systems. Strongly encouraged are proposals of new,
speculative ideas, evaluations of new or known techniques in practical
settings, and discussions of emerging threats and important problems. We
are especially interested in position papers that are radical,
forward-looking, and likely to lead to lively and insightful discussions
that will influence future research that lies at the intersection of
programming languages and security.

The scope of PLAS includes, but is not limited to:
● Compiler-based security mechanisms (e.g. security type systems) or
runtime-based security mechanisms (e.g. inline reference monitors)
● Program analysis techniques for discovering security vulnerabilities
● Automated introduction and/or verification of security enforcement
mechanisms
● Language-based verification of security properties in software, including
verification of
cryptographic protocols
● Specifying and enforcing security policies for information flow and
access control
● Model-driven approaches to security
● Security concerns for Web programming languages
● Language design for security in new domains such as cloud computing and
IoT
● Applications, case studies, and implementations of these techniques

—

Submission Guidelines

We invite both full papers and short papers. For short papers we especially
encourage the submission of position papers that are likely to generate
lively discussion.
● Full papers ​should be at most 11 pages long, plus as many pages as
needed for references and appendices. Papers in this category are expected
to have relatively mature content. Full paper presentations will be 25
minutes each.
● Short papers should be at most 5 pages long, plus as many pages as needed
for references. Papers that present radical, open-ended and forward-looking
ideas are particularly welcome in this category, as are papers presenting
preliminary and exploratory work. Authors submitting papers in this
category must prepend the phrase "Short Paper:" to the title of the
submitted paper. Short paper presentations will be 15 minutes each.

Submissions should be PDF documents formatted according to the CCS 2017
formatting requirements provided at
https://www.sigsac.org/ccs/CCS2017/#format 
. Both full and short papers must
describe work not published in other refereed venues. Accepted papers will
appear in workshop proceedings, which will be distributed to the workshop
participants and be available in the ACM Digital Library.

PLAS welcomes submissions by authors of all nationalities and we do not
wish to exclude any potential authors who may have difficulty traveling due
to recent changes in US immigration practices. We will allow presenting
papers electronically or with non-author presenters in cases where paper
authors are unable to travel to the United States.

—

Workshop co-chairs:

Nataliia Bielova (Inria, France, Co-Chair)
Marco Gaboardi (University at Buffalo, SUNY, USA, Co-Chair)

Program Committee:

Mario Alvim (Universidade Federal de Minas Gerais, Brazil)
Aslan Askarov (Aarhus University, Denmark)
Lujo Bauer (Carnegie Mellon University, USA)
Deepak Garg (MPI Software Systems, Germany)
Kevin Hamlen (University of Texas at Dallas, USA)
Boris Koepf (IMDEA Software Institute, Spain)
Steve Kremer (Loria & Inria, France)
Scott Moore (Harvard University, USA)
Frank Piessens (DistriNet, Katholieke Universiteit Leuven, Belgium)
Omer Tripp (Google, USA)
Danfeng Zhang (Penn State University, USA)