[TYPES/announce] JFLA 2017: Call for Participation

[François Pottier]

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


[This message is intentionally written in French. JFLA 2017 is a
French-speaking conference on functional programming languages.]

   *** Appel à participation, merci de diffuser largement ***


JFLA'2017 (http://jfla.inria.fr/2017/)

Journées Francophones des Langages Applicatifs

   Gourette, Pyrénées, du 4 au 7 janvier 2017


Les incriptions aux JFLAs 2017 sont ouvertes jusqu'au 11 décembre :

http://jfla2017.events-sudcongresconseil.com/register.aspx?e=598

Le programme des Journées est désormais disponible en ligne :

http://jfla.inria.fr/2017/programme.html

Ces journées réunissent concepteurs, utilisateurs et théoriciens ; elles ont
pour ambition de couvrir les domaines des langages applicatifs, de la preuve
formelle, de la vérification de programmes, et des objets mathématiques qui
sous-tendent ces outils. Ces domaines doivent être pris au sens large : nous
souhaitons promouvoir les ponts entre les différentes thématiques.

L'inscription est un forfait qui comprend notamment l'hébergement en pension
complète sur le site des journées et le transfert en car entre Gourette 
et la

gare ou l'aéroport de Pau :
- participant plein tarif, chambre single : 600 euros
- participant plein tarif, chambre twin : 500 euros
- étudiant, chambre twin : 350 euros
- étudiant avec article accepté, chambre twin : gratuit (!)

Nous espérons que vous serez nombreux à participer à ces journées.
Inscrivez-vous dès que possible!

Dates importantes
-

11 décembre 2016 : date limite d'inscription aux journées
4 au 7 janvier 2017 : journées

Cours invités
-

* Guillaume Burel (ENSIIE)
  "Exprimer ses théories en Dedukti, le vérificateur de preuves universel"

* Benjamin Canou (OCamlPro SAS)
  "Comment programmer en OCaml aujourd'hui"

Exposés invités
-

* Damien Doligez (Inria Paris)
  "Zenon"

* Stéphane Lescuyer et Florence Plateau (Prove and Run)
  "Langage et outil pour la preuve d'un micro-noyau"
  (titre exact à préciser)

Comité de programme
---

Julien Signoles   CEA LIST (président)
Sylvie Boldo  Inria Saclay-Île de France, LRI (vice-présidente)
June   Andronick  Data61/CSIRO et UNSW
Anne-Gwenn Bosser ENIB, Lab-STICC
Thomas Gazagnaire Docker
MohamedIguernlala OCamlPro SAS
Frédéric   Loulergue  SICCS, Northern Arizona University
LaurentMounierVerimag, Université Grenoble Alpes
François   PottierInria Paris
SylvainSalvatiUniversité Lille 1
MihaelaSighireanu IRIF, Université Paris 7
Francesco  Zappa Nardeli  Inria Paris

Pour tout renseignement, contacter
  Julien Signoles 

[TYPES/announce] Call for Participation: POPL 2017 and co-located events [early registration deadline approaching]

[David Baelde]

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


** POPL 2017 **

44th ACM SIGPLAN Symposium on Principles of Programming Languages
January 15-21, 2017, Paris, France

The annual Symposium on Principles of Programming Languages is a forum
for the discussion of all aspects of programming languages and
programming systems. Both theoretical and experimental papers are
welcome, on topics ranging from formal frameworks to experience
reports.

The symposium is sponsored by ACM SIGPLAN, in cooperation with
ACM SIGACT and ACM SIGLOG.

Registration for POPL and co-located events is open:

  http://popl17.sigplan.org/attending/registration

Important dates:

  early registration deadline: December 17, 2016
  main conference: January 18-20, 2017
  co-located events:   January 15-17 and 21, 2017

Attendees can register their interest to find a roommate (without
sharing their contact information publicly) through ConferenceShare:

  http://conferenceshare.co

For more details on tutorials, invited speakers, programs
and associated events, please visit our website:

  http://popl17.sigplan.org/

Co-hosted Conferences:
CPP 2017
VMCAI 2017

Co-hosted Symposium:
PADL 2017

Co-hosted Workshops:
PPS 2017
CoqPL 2017
N40AI
OBT 2017
PEPM 2017
PLMW
PiP 2017
RDP 2017
SCM 2017
TTT 2017

[TYPES/announce] Partial Evaluation & Program Manipulation (PEPM'17): Call for Participation

[Jeremy Yallop]

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

CALL FOR PARTICIPATION
Workshop on PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM 2017)

http://conf.researchr.org/home/PEPM-2017

Paris, France, January 16th - 17th, 2017
(co-located with POPL 2017)

Registration


http://popl17.sigplan.org/attending/registration

Early registration deadline: Saturday 17th Dec 2016

Programme
-

Monday 16th January

09:00-10:00: Keynote

   Compiling Untyped Lambda Calculus to Lower-Level Code by Game
Semantics and Partial Evaluation
 Neil D. Jones (with Daniil Berezun)

10:30-12:00: Programming languages

   Lightweight Soundness for Towers of Language Extensions
 Alejandro Serrano, Jurriaan Hage

   Detecting code clones with gaps by function applications
 Tsubasa Matsushita, Isao Sasano

   PEG Parsing in Less Space Using Progressive Tabling and Dynamic Analysis
 Fritz Henglein, Ulrik Terp Rasmussen

14:00-15:30: Tutorial and Poster Session

   Idris, Inside-Out: A Tutorial on Extending Idris in Idris
  David Christiansen

   Language-integrated Query with Ordering, Grouping and Outer Joins (poster)
  Tatsuya Katsushima, Oleg Kiselyov

16:00-17:00: Transformation (part I)

   Verification of Code Generators via Higher-Order Model Checking
  Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi

   Interactive data representation migration: Exploiting program
dependence to aid program transformation
  Krishna Narasimhan, Julia Lawall, Christoph Reichenbach

Tue 17th January

09:00-10:00: Tutorial

   Reversible computing from a programming language perspective
  Robert Glück

10:30-12:00: Types

   Cost versus Precision for Approximate Typing for Python
  Levin Fritz, Jurriaan Hage

   Refining types using type guards in TypeScript
  Ivo Gabe de Wolff, Jurriaan Hage

   Predicting Resource Consumption of Higher-Order Workflows
  Markus Klinik, Jurriaan Hage, Jan Martin Jansen, Rinus Plasmeijer

14:00-15:30: Tutorial

   Practical Partial Evaluation for Language Implementation with Graal & Truffle
  Gilles Duboscq

16:00-17:00: Transformation (part II)

   Functional Parallels of Sequential Imperatives
  Tiark Rompf, Kevin J. Brown

   A Functional Reformulation of UnCAL Graph-Transformations: Or,
Graph Transformation as Graph Reduction
  Kazutaka Matsuda, Kazuyuki Asada

[TYPES/announce] Three open faculty positions (tenure-track or tenured) at MPI-SWS

[Derek Dreyer]

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

[Note for Types folks: Although we already have several faculty in PL
and verification, we are quite open at this point to hiring more.]

At the Max Planck Institute for Software Systems (MPI-SWS), we are
looking to fill three tenure-track (and/or tenured) faculty positions
starting in October 2017. Our faculty positions combine the benefits
of academia and research labs: full academic freedom combined with
generous, perpetual base funding to lead a team of students and
postdocs.  We would like to invite applications from outstanding
applicants in all areas pertaining to the theory and practice of
software systems, including security and privacy, embedded and mobile
systems, distributed and parallel systems, computational social
science, legal, economic, and social aspects of computing, NLP,
machine learning, information and knowledge management, programming
languages, algorithms and logic, and verification.

Candidates should hold (or expect to receive by the end of 2017) a
doctoral degree in computer science or a related discipline. To
receive full consideration, applications should be received by
December 16, 2016.

Applicants at all levels of seniority should apply at:
https://apply.mpi-sws.org.

Further information about our institute and the positions can be found
at our website (https://www.mpi-sws.org). I would also be happy to
answer any informal queries.

Sincerely,
Derek Dreyer
Tenured Faculty, MPI-SWS

[TYPES/announce] Associate/Assistant Professor in Programming Languages at the Technical University of Denmark

[Alberto Lluch Lafuente]

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

Dear colleagues,

There is an open position in the section for Formal Methods at the
Department of Applied Mathematics and Computer Science of Technical
University of Denmark. The position is at the assistant or associate
professor level within the area of implementation of programming languages.

The date for application is on February 5'th and full details are available
at

http://www.compute.dtu.dk/english/about_us/vacant_jobs/job?id=2be9221f-100d-4654-ae96-2e46aae2e447

Our vision is that Formal Methods offer key methods for constructing a
reliable and trustworthy IT infrastructure. We have competences within the
modelling, analysis and realisation of systems that cover semantics,
program analysis, model checking, language based security, and software
tools. We hope to attract a brilliant candidate in programming language
implementation that will engage in our research and teaching.

More details on our section for Formal Methods can be found at

http://www.compute.dtu.dk/english/research/fm/

Please do not hesitat to contact us for inquires:
- Hanne Riis Nielson 
- Flemming Nielson 
- Sebastian Alexander Mödersheim 
- Alberto Lluch Lafuente 

Best wishes,

Alberto, Hanne, Flemming, Sebastian

[TYPES/announce] CoqPL 2017: Call for Participation [registration is open]

[Emilio Jesús Gallego Arias]

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

The 3rd International Workshop on Coq for Programming Languages
Associated to POPL 2017

The CoqPL workshop provides an opportunity for programming languages
researchers to meet and interact with one another and members from the
core Coq development team.

Important dates:

- early registration deadline: December 17, 2016
- workshop: January 21, 2017

Important links:

- Program URL:
  http://conf.researchr.org/track/CoqPL-2017/main#program

- Registration URL:
  http://popl17.sigplan.org/attending/registration

[TYPES/announce] Postdoc position in the area of formal verification

[Taolue Chen]

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

[Apology for cross-posting.]

Applications are invited for a Postdoctoral Research Fellow position
working on formal verification. The work is being funded by EPSRC.

The aim of the project is to carry out perturbation analysis for
quantitative verification, i.e.,

(1) to analyse how the verification result is affected by the perturbation
of parameters and to provide a quantitative measure thereof; and
(2) to develop software tools to facilitate the perturbation analysis. The
toolkit will be employed to conduct case studies on real-world problems.

For some background on the kind of work, see the following papers

http://www.eis.mdx.ac.uk/staffpages/taoluechen/pub-papers/fase16.pdf
http://www.eis.mdx.ac.uk/staffpages/taoluechen/pub-papers/TSE16.pdf
http://www.eis.mdx.ac.uk/staffpages/taoluechen/pub-papers/concur14.pdf


The postdoc will be supervised by Dr Taolue Chen and be based in the
Department of Computer Science at Middlesex University London, UK. We offer
a competitive salary (in the range of £36,179 to £41,560 per annum). The
post is available for one year.

To apply, you must hold (or be close to achieving) a PhD in Computer
Science or a closely related discipline. You should have demonstrated your
research competence through high-quality and high-impact publications in
formal verification.

Informal enquiries are strongly encouraged and should be made to:

* Dr Taolue Chen (t.c...@mdx.ac.uk, taolue.c...@gmail.com)
 http://www.eis.mdx.ac.uk/staffpages/taoluechen/