[TYPES/announce] Chalmers Online Functional Programming Seminar Series (TODAY: Benjamin Pierce!)

[Benjamin C. Pierce]

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

A reminder of today's seminar by Benjamin Pierce. 16.00.
Backtracking Generators for Random Testing.

Last week we had 720 people who tuned in to Simon Peyton Jones! Unfortunately, 
we had severe problems using Zoom webinar technology (which was dimensioned in 
our license for up to 1000 people, but Zoom was just not up to the task).

This week we will use YouTube Live streaming and sli.do for questions. All 
relevant links are on chalmersfp.org . See you there!

Mary Sheeran, John Hughes, and Koen Claessen

[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] Guide to best practices for virtual conferences

[Benjamin C. Pierce]

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

[TL;DR: Please help circulate a new guide for organizers of virtual 
conferences.]

Dear colleagues,

The Association for Computing Machinery recently chartered a Presidential Task 
Force to gather and disseminate guidance on best practices for virtual 
conferences, aimed at the many conference organizers moving their events online 
right now. 

The task force report, Virtual Conferences: A Guide to Best Practices 
, is now available on the ACM web site 
  It offers a comprehensive survey of 
issues, organizational strategies, and technology platforms for successful 
virtual meetings.

We hope that you and others in your field will find this report useful. If you 
do, we would love to hear about it! And naturally if you have any suggestions 
for improvement, we would love to hear those too; the PDF document linked above 
includes a pointer to a live Google Doc where you can leave suggestions and 
comments if you like. If you have recently organized a virtual conference or 
are organizing one now, we would especially like to include your experiences 
(how you organized it, how it went, what people thought, a summary of any 
post-conference survey results, your advice for future conferences, etc.) and 
add it (or better yet a pointer to it) to the appendix that we’ve provided for 
such experience reports.

Finally, can you please help us make sure this guide reaches the people that 
need it by forwarding this announcement within your networks (especially, of 
course, to current conference organizers)? 

Many thanks!

 Benjamin Pierce

…on behalf of the entire task force:

Crista Videira Lopes , University of 
California, Irvine, USA (Task Force Co-chair)
Jeanna Matthews , Clarkson University, 
USA (Task Force Co-chair, member of ACM Council, Former SGB Chair)
Benjamin Pierce , University of 
Pennsylvania, USA (Task Force Executive Editor, SIGPLAN Vice Chair, chair of 
SIGPLAN ad hoc committee on climate change 
)

Blair MacIntyre , Georgia Tech, USA (Chaired IEEE 
VR 2020)
Gary Olson , University of California, Irvine, USA 
(Former SIGCHI Treasurer; Chair of CSCW Steering Committee, chaired CHI, CSCW, 
DIS, and many non-ACM conferences)
Rob Lindeman 
,
 University of Canterbury, NZ (Chaired IEEE VR 2010)
Francois Guimbretiere , Cornell 
University, USA (Chaired UIST 2019)
Srinivasan Keshav 
, University of 
Cambridge, UK (Former SIGCOMM Chair)

Ex-officio members:
Vicki Hanson  (ACM CEO, Former ACM President)
Pat Ryan (ACM COO)
Donna Cappo (ACM Director of SIG Services)

[TYPES/announce] Postdoc opening at the University of Pennsylvania

[Benjamin C. Pierce]

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

The University of Pennsylvania's Accountable Protocol Customization (APC) 
project is a new multi-disciplinary effort funded by the Office of Naval 
Research (ONR) as part of its Total Platform Cyber Protection (TPCP) program. 
The goal is to develop tools and reasoning principles for protocol 
customization aimed at software de-bloating, by identifying lean protocol 
subsets that are sufficient to meet the functional and security needs of 
relevant clients and servers while preserving backward compatibility. 
Customization can also support protocol dialects that modify the original 
protocol standard in settings  where backward compatibility is not a strict 
requirement. A central project theme is ensuring that customization is 
“accountable” — i.e. carefully vetting properties of customized protocols by 
tightly coupling protocol customization operations with rigorous formal 
analysis and machine-checked proofs in the Coq proof assistant.  A particular 
target area is modern web protocols such as HTTP2 and TLS. 

Our APC project, in collaboration with Carnegie-Mellon University and Stanford 
University, brings together researchers with expertise in formal methods, 
programming languages, distributed systems, and network security. 

The APC team at Penn has funding for one post-doctoral researcher. This is a 
one-year position, based in Philadelphia, with the option of a second year 
subject to mutual agreement and funding availability. The postdoc will have the 
freedom to lead individual projects as well as working with a strong team of 
researchers including Ph.D., Masters, and undergraduate students.

We seek applicants with expertise in at least one, preferably two or more, of 
the following areas: formal methods, programming languages, distributed 
systems, and network security. Applicants should email their CV and a research 
statement to Dr. Boon Thau Loo (boon...@seas.upenn.edu 
<mailto:boon...@seas.upenn.edu>) and also ask two or three references to email 
letters of recommendation to Dr. Loo.

For more information, please feel free to contact any of the APC Principal 
Investigators: 
Boon Thau Loo (boon...@seas.upenn.edu <mailto:boon...@seas.upenn.edu>)
    Benjamin C. Pierce (bcpie...@seas.upenn.edu)
Andre Scedrov (sced...@seas.upenn.edu)
Steve Zdancewic (ste...@seas.upenn.edu) 

[TYPES/announce] Postdoc positions at the University of Pennsylvania

[Benjamin C. Pierce]

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

PENN’S PL CLUB IS LOOKING FOR POSTDOCS

The University of Pennsylvania’s PL group is looking to hire multiple 
postdoctoral researchers to work on projects related to verification, software 
specification, and security.

START DATES: Negotiable

DURATION: All positions are one year, with the possibility of extension to a 
second year.

QUALIFICATIONS: Applicants should have a Ph.D. in computer science and a strong 
background in one or more topics related to 
formal verification and specification
programming languages
type systems and semantics
the Coq theorem prover
the specific project topics described below.

APPLICATION PROCEDURE:
Upload a CV, statement of interest, and the names of three letter writers to: 
https://goo.gl/forms/SMu8KmtdHjXKnqWF3 
Direct your letter writers to submit their letters here: 
https://goo.gl/forms/ElgimgzvDh4C2scu1 
Contact Steve Zdancewic (ste...@cis.upenn.edu ) or 
Benjamin Pierce (bcpie...@cis.upenn.edu ) if you 
have any questions.
New applications will be considered starting immediately and will be considered 
until all the positions are filled.

Successful applicants will join the University of Pennsylvania’s PL Club with 
opportunities to collaborate on the DeepSpec project and other ongoing 
activities.


POTENTIAL RESEARCH PROJECTS

DeepWeb - A Formally Verified Web Server

Penn is coordinating a large-scale verification effort that combines 
technologies from across the DeepSpec project with the aim creating a verified 
web server: the high-level specification is in terms of the HTTP protocol, and 
the implementation will be high-performance C software (verfied using 
Princeton’s VST) hosted by Yale’s CertiKOS, which will itself be run on top of 
MIT’s verified implementation of the Risc V hardware. This project will tie 
together specification, verification, and testing across multiple levels of 
abstraction.

QuickChick - Property-Based Testing for Coq

The QuickChick project investigates the interplay between formal specification 
/ verification and property-based random testing a la Haskell QuickCheck. The 
QuickChick tool (a QuickCheck-like testing framework for Coq) is heavily used 
in the DeepSpec project, for example as the specification framework for an 
executable formal specification of HTTP and related protocols. We are 
experimenting with using this specification as a bug-finding tool, both for 
industrial web servers and for initial prototypes of our own server. This 
requires addressing both foundational and engineering challenges, in the 
testing technology and in the creation of specifications that are suitable for 
both verification and testing.

Programming Languages for Differential Privacy

Penn boasts a longstanding and energetic collaborative research effort on 
putting new privacy technologies – particular statistical techniques such as 
differential privacy – into practice, involving faculty, students, and postdocs 
from programming languages, distributed systems, and algorithms, and machine 
learning. Topics of interest include privacy-protecting type systems and static 
analyses, distributed implementations of private algorithms, program logics for 
privacy, and formal verification of randomized algorithms.


THE UNIVERSITY OF PENNSYLVANIA

Penn’s department of Computer and Information Science offers a vibrant research 
environment with a long tradition of excellence in programming languages and 
related areas. We are located in Philadelphia, a city that offers a rich array 
of cultural, historical, and nightlife attractions, parks and outdoor 
recreation, convenient public transportation, and affordable housing.

[TYPES/announce] PhD positions at Penn in PL and Formal Methods

[Benjamin C. Pierce]

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

The Programming Languages and Formal Methods group at the University of 
Pennsylvania invites interested students to apply to our PhD program.  We 
conduct research on a broad range of topics spanning language design, 
programming systems, logic and verification.  The group is led by five faculty 
with diverse expertise: Rajeev Alur, Mayur Naik, Benjamin Pierce, Stephanie 
Weirich, and Steve Zdancewic. Our ongoing research projects include The Science 
of Deep Specification (deepspec.org ), 
Computer-Augmented Programming (excape.cis.upenn.edu 
), Verified LLVM 
(www.cis.upenn.edu/~stevez/vellvm ), 
Dependent Types for Haskell (www.haskell.org ), AI for 
Programming Systems (petablox.org ), and a range of other 
topics.  

Penn is located in Philadelphia, a vibrant and cosmopolitan city with many 
socializing, dining, athletic, and entertainment options, and easy 
transportation to most of the eastern seaboard. The Computer and Information 
Science department (www.cis.upenn.edu ) provides a 
world-class environment for doing basic as well as inter-disciplinary research. 
 The PL+FM group is regularly ranked  
as one of the top programs worldwide. 

Prospective students should apply to the PhD program in Computer and 
Information Science at
http://www.cis.upenn.edu/prospective-students/graduate/applying.php 
 by 
December 15, 2017.

[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] Last call: DeepSpec Summer School, July 13-28, 2017

[Benjamin C. Pierce]

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

The first DeepSpec Summer School on Verified Systems will be held in 
Philadelphia from July 17 to 28, 2017, preceded by an introductory Coq 
Intensive from July 13 to 15.

The second week is currently full, but there are a few places left for 
self-funded participants in the first week (Leroy, Pierce, Weirich, and 
Zdancewic) and the preceding Coq Intensive.

The deadline for registration and hotel booking is next Monday, June 12th.

Overview
Can critical systems be built with no bugs in hardware, operating systems, 
compilers, crypto, or other key components? It may seem a pipe dream, but the 
past decade has seen explosive advances in the technology required to realize 
it. This summer school aims to give participants a wide-ranging overview of 
several ambitious projects currently underway in this space. 

Participants will complete the summer school with a thorough understanding of 
the conceptual underpinnings of these projects plus considerable hands-on 
experience with state-of-the-art tools for building verified systems.

Dates
The summer school will open with a three-day intensive course on Coq 
fundamentals, for participants who are new to Coq. The main lectures take place 
during the weeks of July 17 and 24. 

July 13-15 (Thu-Sat)Coq intensive 
July 17-21  Week 1
July 24-28  Week 2
Lecturers and Topics
Andrew AppelVerified functional algorithms 
Adam Chlipala   Program-specific proof automation
Frans Kaashoek & Nickolai Zeldovich Certifying software with crashes 
Xavier LeroyThe structure of a verified compiler
Benjamin Pierce Property-based random testing with QuickChick 
Zhong Shao  CertiKOS: Certified kit operating systems
Stephanie Weirich   Language specification and variable binding
Steve Zdancewic Vellvm: Verifying the LLVM 
Prerequisites
The DeepSpec summer school is aimed at a wide range of participants, including 
graduate students, academics, and industrial engineers and researchers. 

The Coq proof assistant will serve as a lingua franca for all the lectures. 
Participants who are not already familiar with Coq at the level of Software 
Foundations  should 
plan on attending the Coq Intensive before the summer school.

Details
Please see https://deepspec.org/event/dsss17/announcement.html 
 for further information 
and a link to the registration form.

[TYPES/announce] [CSF-attendees] DeepSpec Summer School, July 13-28, 2017 -- call for applications

[Benjamin C. Pierce]

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

The first DeepSpec Summer School on Verified Systems will be held in 
Philadelphia from July 17 to 28, 2017, preceded by an introductory Coq 
Intensive from July 13 to 15.  

Applications are now being accepted !

Overview
Can critical systems be built with zero bugs in critical components such as 
hardware, operating systems, compilers, or crypto? It may seem a pipe dream, 
but in fact the past decade has seen explosive advances in the technology 
required to realize it.

This summer school aims to give participants a wide-ranging overview of several 
ambitious projects currently underway in this space. 

Participants will complete the summer school with a thorough understanding of 
the conceptual underpinnings of these projects plus considerable hands-on 
experience with state-of-the-art tools for building verified systems.


Dates
The summer school will open with a three-day intensive course on Coq 
fundamentals, for participants who are new to Coq. The main lectures take place 
during the weeks of July 17 and 24. 

July 13-15 (Thu-Sat)Coq intensive 
July 17-21  Week 1
July 24-28  Week 2
Lecturers and Topics
Andrew AppelVerified functional algorithms 
Adam Chlipala   Program-specific proof automation
Frans Kaashoek & Nickolai Zeldovich Certifying software with crashes 
Xavier LeroyThe structure of a verified compiler
Benjamin Pierce Property-based random testing with QuickChick 
Zhong Shao  CertiKOS: Certified kit operating systems
Stephanie Weirich   Language specification and variable binding
Steve Zdancewic Vellvm: Verifying the LLVM 

Prerequisites
The DeepSpec summer school is aimed at a wide range of participants, including 
graduate students, academics, and industrial engineers and researchers. 

The Coq proof assistant will serve as a lingua franca for all the lectures. 
Participants who are not already familiar with Coq at the level of Software 
Foundations  should 
plan on attending the Coq Intensive before the summer school.


Costs and Financial Aid
The total cost (for lectures, meals, and dormitory lodging) is expected to be 
roughly $2000 per participant.

Substantial subsidies are available, courtesy of the NSF (thank you!), for 
students requiring financial assistance to attend. More details will be 
announced when applications open.

Applications
Applications are now open (here) !  
Applications received by Feb 15 will be given equal consideration; applications 
received after Feb 15 will be considered on a space-available basis.

[TYPES/announce] DeepSpec Summer School, July 13-28, 2017

[Benjamin C. Pierce]

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

The first DeepSpec Summer School on Verified Systems will be held in 
Philadelphia from July 17 to 28, 2017, preceded by an introductory Coq 
Intensive from July 13 to 15.

Overview
Can critical systems be built with no bugs whatsoever in hardware, operating 
systems, compilers, crypto, or other key components? It may seem a pipe dream, 
but in fact the past decade has seen explosive advances in the technology 
required to realize it.

This summer school aims to give participants a wide-ranging overview of several 
ambitious projects currently underway in this space. 

Participants will complete the summer school with a thorough understanding of 
the conceptual underpinnings of these projects plus considerable hands-on 
experience with state-of-the-art tools for building verified systems.

Dates
The summer school will open with a three-day intensive course on Coq 
fundamentals, for participants who are new to Coq. The main lectures take place 
during the weeks of July 17 and 24. 

July 13-15 (Thu-Sat)Coq intensive 
July 17-21  Week 1
July 24-28  Week 2
Lecturers and Topics
Andrew AppelVerified functional algorithms 
Adam Chlipala   Program-specific proof automation
Frans Kaashoek & Nickolai Zeldovich Certifying software with crashes 
Xavier LeroyThe structure of a verified compiler
Benjamin Pierce Property-based random testing with QuickChick 
Zhong Shao  CertiKOS: Certified kit operating systems
Stephanie Weirich   Language specification and variable binding
Steve Zdancewic Vellvm: Verifying the LLVM 
Prerequisites
The DeepSpec summer school is aimed at a wide range of participants, including 
graduate students, academics, and industrial engineers and researchers. 

The Coq proof assistant will serve as a lingua franca for all the lectures. 
Participants who are not already familiar with Coq at the level of Software 
Foundations  should 
plan on attending the Coq Intensive before the summer school.

Costs and Financial Aid
The total cost (for lectures, meals, and dormitory lodging) is expected to be 
roughly $2000 per participant.
Substantial subsidies are available, courtesy of the NSF (thank you!), for 
students requiring financial assistance to attend. More details will be 
announced when applications open.

Applications
Applications will be accepted beginning on Jan 15; please subscribe to the 
DeepSpec mailing list 
 to receive an 
announcement when applications open. Applications received by Feb 15 will be 
given equal consideration; applications received after Feb 15 will be 
considered on a space-available basis.

[TYPES/announce] Postdoc position at Penn on the DeepSpec project

[Benjamin C. Pierce]

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


Join Penn as a postdoc on the DeepSpec  project! 

Outstanding postdocs with interests in programming languages, formal 
verification, and systems software are invited to join the programming 
languages group at Penn!  We are currently seeking researchers as part of “The 
Science of Deep Specification,” an NSF-funded Expedition in Computing.  

The goal of DeepSpec is to catalyze the adoption of deep specification 
techniques, through a tightly integrated combination of focused research, 
course development, and community building.  At Penn, Steve Zdancewic leads the 
Vellvm  project, which provides a Coq 
specification of the LLVM intermediate representation. In this Expedition, 
Vellvm will serve as a testbed for experimenting with proof-engineering 
techniques and as a component of a larger system involving many deep 
specifications. Handling deep specifications at such a large scale (and that 
evolve over time, as LLVM’s must) will require significant technical advances. 
Stephanie Weirich leads the CoreSpec  
project, which seeks to develop a Coq specification of the core language of the 
Glasgow Haskell Compiler (GHC).  This part of the DeepSpec project will extend 
the breadth of the connected network of specifications to include a 
industrial-strength high-level programming language.  Benjamin Pierce leads the 
QuickChick  project, focused on 
property-based testing of deep specifications.  The goal of this part of the 
DeepSpec research is to accelerate the development of deeply specified software 
by supporting a smooth transition between automated random testing and full 
formal verification.  Another strong focus of work at Penn will be on the role 
of deep specifications in modernizing undergraduate curricula in traditional 
core subjects such as operating systems and compilers.

These threads are closely connected to the other components of the DeepSpec 
consortium. In particular, this work will be done in the context of 
interconnected systems, interacting with and building on verified operating 
systems (CertiKOS, Yale), verified C compilers (CompCert and Verifiable C, 
Princeton), and verified hardware programming (Kami, MIT).  

The ideal candidate will have a PhD in Computer Science or a related field and 
experience with the Coq proof assistant or a similar tool. To ensure full 
consideration, please send a CV and research statement to Benjamin Pierce 
(bcpie...@cis.upenn.edu ), and arrange for at 
least three letters of reference to be sent to the same address, by February 
15, 2016.  

The University of Pennsylvania  is an equal opportunity employer. All qualified 
applicants will receive consideration for employment without regard to race, 
color, religion, sex, national origin, disability status, protected veteran 
status, or any other characteristic protected by law. 

More information about the DeepSpec project is available at deepspec.org 
.

Looking forward to your application,

 Benjamin Pierce
 Stephanie Weirich
 Steve Zdancewic

[TYPES/announce] Faculty position at Penn in Formal Methods

[Benjamin C. Pierce]

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

The Department of Computer and Information Science at the University of 
Pennsylvania (http://www.cis.upenn.edu) is recruiting faculty for Fall 2016, 
with Formal Methods as a priority area.  We are particularly interested in 
junior researchers whose prior work focuses on either security or embedded 
systems and who will complement our existing strengths in cyber-physical 
systems (http://precise.seas.upenn.edu/) and programming languages 
(http://www.cis.upenn.edu/~plclub/).

To apply, please visit https://facultysearches.provost.upenn.edu/postings/663

[TYPES/announce] Postdoc opening in PL and security at University of Pennsylvania

[Benjamin C. Pierce]

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

Applications are invited for a postdoc position with the CRASH/SAFE project at 
the University of Pennsylvania.

CRASH/SAFE is an ambitious effort to design new computer systems that are 
highly resistant to cyber-attack.  It offers a rare opportunity to rethink the 
hardware / OS / software stack from a completely clean slate, with no legacy 
constraints whatsoever.  Specifically, we aim to build a suite of modern 
operating system services that embodies and supports fundamental security 
principles—including separation of privilege, least privilege, and mutual 
suspicion—down to its very bones, without compromising performance.  Achieving 
this goal demands an integrated effort focusing on (1) processor architectures, 
(2) operating systems, (3) formal methods, and (4) programming languages and 
compilers -- coupled with a co-design methodology in which all critical system 
layers are designed together, with a ruthless insistence on simplicity, 
security, and verifiability at every level.  The project is joint with Harvard, 
Northeastern, and BAE Systems.  More information and papers describing project 
results can be found at http://www.crash-safe.org.  

The ideal candidate will have a Ph.D. in Computer Science, a combination of 
strong theoretical and practical interests, and expertise in two or more of the 
following areas: programming languages, security, formal verification, 
operating systems, and hardware design.

The position is for one year in the first instance, with possible renewal for 
one or more additional years.  Starting date is negotiable; salary commensurate 
with experience.  Applications from women and members of other 
under-represented groups are particularly welcome.

Penn's department of Computer and Information Science offers a vibrant research 
environment with a long tradition of excellence in programming languages and 
related areas.  We are located in Philadelphia, a city that offers a rich array 
of cultural, historical, and nightlife attractions, parks and outdoor 
recreation, convenient public transportation, and affordable housing.

To apply, please send a CV, research statement, and the names of four people 
who can be asked for letters of reference to Benjamin Pierce 
(bcpie...@cis.upenn.edu).

[TYPES/announce] Japanese translation of Software Foundations

[Benjamin C. Pierce]

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

Friends and colleagues,

As many of you know, Software Foundations 
(http://www.cis.upenn.edu/~bcpierce/sf/) is a electronic textbook introducing 
functional programming, Coq proof development, and the theory of programming 
languages, written entirely in Coq.  It has been developed over the past five 
years by a large group of contributors and is widely used for both teaching and 
self-study.

Today, I am delighted to announce that, thanks to a dedicated team of 
translators, Software Foundations can now be read in Japanese!  

http://proofcafe.org/sf

Many thanks to the translation team for this effort!

  - Akihiro Umemura
  - Koji Katayama
  - Hiroki Mizuno
  - Daichi Oohashi
  - Moe Masuko
  - Yoshihiro Imai

Share and enjoy,

- Benjamin

[TYPES/announce] TLDI 2012 - Call for Papers and Contributed Talks (updated)

[Benjamin C. Pierce]

 digital library.

 __

Important Dates

  Submission deadline October 10, 2011 (Monday)
  NotificationNovember 10, 2011 (Thursday)
  WorkshopJanuary 28, 2012 (Saturday)

 __

Program Chair:

  Benjamin C. Pierce
  University of Pennsylvania
  bcpierce atsign cis dot upenn dot edu

Program Committee:

  Jonathan Aldrich CMU
  Adam ChlipalaMIT
  Pierre-Malo Deniélou Imperial College London
  Kathleen Fisher  Tufts University
  Chris Hawblitzel Microsoft Research (Redmond)
  Dan Licata   CMU
  Greg Morrisett   Harvard University
  Benjamin C. Pierce   University of Pennsylvania
  Dimitrios Vytiniotis Microsoft Research (Cambridge)

Steering Committee:

  Amal Ahmed   Indiana University
  Nick Benton  Microsoft Research, Cambridge
  Derek Dreyer MPI-SWS
  Andrew Kennedy   Microsoft Research, Cambridge
  Francois Pottier INRIA Paris-Rocquencourt
  Stephanie WeirichUniversity of Pennsylvania

[TYPES/announce] Workshop on Bidirectional Transformations (BX 2012)

[Benjamin C. Pierce]

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

  CALL FOR PAPERS

  First International Workshop on
  Bidirectional Transformations (BX 2012)

  Tallinn, Estonia
Sun, March 25, 2012

(co-located with ETAPS 2012)

 http://www.program-transformation.org/BX12
===


INVITED SPEAKERS:

* Juan de Lara (Autonomous University of Madrid, Spain)
* second invited speaker still to be decided


IMPORTANT DATES:

* Paper submission:Mon, December 19, 2011
* Author notification: Tue, January 24, 2012
* Camera-ready papers: Sun, February 5, 2012

To facilitate smooth organization of the review process, authors are
asked to submit a short abstract by December 12, 2011.


SUBMISSION CATEGORIES:

* Regular submissions (max. 15 pages, formal proceedings)
* Short papers(max. 8 pages, informal proceedings)
* Lightning talks (extended abstract)

Submissions can be in LNCS or EC-EASST style.

More details can be found on the webpage.


PROCEEDINGS:

There will be formal proceedings containing all accepted regular papers,
published as a volume of EC-EASST (Electronic Communications of the
European Association of Software Science and Technology,
http://journal.ub.tu-berlin.de/eceasst). Short papers will be included
in informal proceedings distributed at the workshop, and their authors
may be invited to extend their contribution to a full paper for
inclusion in the formal proceedings.


SCOPE:

Bidirectional transformations (bx) are a mechanism for maintaining the
consistency of two (or perhaps more) related sources of information.
Such sources can be databases, software models, documents, or their
abstract models like graphs or trees. The methodologies used for bx
range from classical program transformation to graph transformation
techniques, from ad-hoc techniques for data synchronization to the
development of domain-specific languages and their integration. We also
solicit papers on model/metamodel co-evolution, which is a different yet
closely related subject.

The aim of the workshop is to bring together researchers, from all
relevant areas, interested in bidirectional transformations from
different perspectives, such as: language-based approaches,
software/model transformations, and data/schema co-evolution.

Topics of interest for BX 2012 include, but are not limited to:

* (coupled) software/model transformations
* software-model synchronization
* data-schema co-evolution and data synchronization
* consistency analysis
* language-based approaches
* analysis/classification of requirements for bx technologies
* case studies and tool support
* comparison of bx technologies
* efficiency of algorithms and benchmarks

Regular submissions (11-15 pages) can be:

* research papers providing new concepts and results
* position papers and research perspectives
* papers that apply bx in new domains
* papers closing gaps between formal concepts and application scenarios

For details about short papers and lightning talks, please consult the
webpage.


PROGRAM CO-CHAIRS:

* Frank Hermann (Technical University of Berlin, Germany;
University of Luxembourg, Luxembourg)
* Janis Voigtländer (University of Bonn, Germany)


PROGRAM COMMITTEE MEMBERS:

* Paolo Atzeni (Roma Tre University, Italy)
* Benjamin Braatz (University of Luxembourg, Luxembourg)
* Anthony Cleve (University of Namur, Belgium)
* Alcino Cunha (University of Minho, Portugal)
* Carlo Curino (Massachusetts Institute of Technology, USA)
* Davide Di Ruscio (University of L'Aquila, Italy)
* Zinovy Diskin (University of Waterloo, Canada)
* Ulrike Golas (Zuse Institute Berlin, Germany)
* Ekkart Kindler (Technical University of Denmark, Denmark)
* Kazutaka Matsuda (Tohoku University, Japan)
* Fernando Orejas (Technical University of Catalonia, Spain)
* Benjamin Pierce (University of Pennsylvania, USA)
* Andy Schürr (Technical University of Darmstadt, Germany)
* Perdita Stevens (University of Edinburgh, UK)
* James Terwilliger (Microsoft, USA)
* Antonio Vallecillo (University of Málaga, Spain)
* Yingfei Xiong (University of Waterloo, Canada)

[TYPES/announce] New release of Software Foundations text

[Benjamin C. Pierce]

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

I'm delighted to announce that the Software Foundations team has recently 
released a new revision of our online textbook:

 http://www.cis.upenn.edu/~bcpierce/sf/

The book covers a semester-long course on basic Coq usage, constructive logic, 
and core topics in the theory of programming languages.  It is being used for 
graduate and advanced undergraduate courses at several institutions, as well as 
by many individuals for self-study.  The main novelty is that every line is 
formalized: the whole book is a Coq script.

Enjoy,

- Benjamin

[TYPES/announce] CRASH/SAFE postdoc opportunities at Penn, Harvard, and Northeastern

[Benjamin C. Pierce]

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

[A more detailed version of the announcement I posted a few weeks ago. --BCP]

Applications are invited for postdoc positions in the areas of programming
languages, operating systems, verification, and hardware design at the
University of Pennsylvania, Harvard University, and Northeastern University.

The hosting project, called SAFE (Semantically Aware Foundation
Environment), is part of CRASH, a larger DARPA-funded effort to design new
computer systems that are highly resistant to cyber-attack, can adapt after
a successful attack in order to continue rendering useful services, learn
from previous attacks how to guard against and cope with future attacks, and
can repair themselves after attacks have succeeded.  It offers a rare
opportunity to rethink the hardware/OS/software stack from a completely
clean slate, with no legacy constraints whatsoever.

Specifically, the SAFE project aims to build a suite of modern operating
system services that embodies and supports fundamental security
principles—including separation of privilege, least privilege, and mutual
suspicion—down to its very bones, without compromising performance.
Achieving this goal demands a co-design methodology in which all critical
system layers are designed together, with a ruthless insistence on
simplicity, security, and verifiability at every level -- an integrated
effort focusing on (1) processor architectures, (2) operating systems, (3)
formal methods, and (4) programming languages and compilers.

The ideal candidate will have a Ph.D. in Computer Science, a combination of
strong theoretical and practical interests, and expertise in two or more of
the following areas: programming languages, security, formal verification,
operating systems, and hardware design.  Applications from women and other
under-represented groups are particularly welcome.

Further details:
 - We expect to offer five positions in the first year -- three at Penn, one
   at Harvard, and one at Northeastern -- with varying duties, salary, and
   desired expertise.  
 - Positions are for one year in the first instance, with possible
   renewal up to four years.  
 - Review of applications is ongoing and will and continue until
   positions are filled.
 - Starting date is negotiable, but we'd ideally like to have people in place
   within a few months.

Background reading:
 SAFE white paper:
   http://www.cis.upenn.edu/~bcpierce/papers/SAFEwhitepaper.pdf
 CRASH BAA: 
   https://www.fbo.gov/utils/view?id=82f6068978da5339752c89d2f65d89ca

To apply, please send a CV, research statement, and the names of three
people who can be asked for letters of reference to Benjamin Pierce
(bcpie...@cis.upenn.edu).  Inquiries can be directed to any of the PIs:

  Andre Dehon (Penn)
  Greg Morrisett (Harvard)
  Benjamin Pierce (Penn)
  Olin Shivers (Northeastern)
  Jonathan Smith (Penn)