[TYPES/announce] Graphical Models for Security (GraMSec 2017) co-located with CSF 2017

2017-05-04 Thread Barbara Kordy

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

GraMSec 2017 - call for papers

The Fourth International Workshop on Graphical Models for Security
Santa Barbara, CA, USA - August 21, 2017

http://gramsec.uni.lu
Co-located with CSF 2017
LNCS proceedings confirmed

SCOPE
Graphical security models provide an intuitive but systematic approach 
to analyze security weaknesses of systems and to evaluate potential 
protection measures. Cyber security researchers, as well as security 
professionals from industry and government, have proposed various 
graphical security modeling schemes. Such models are used to capture 
different security facets (digital, physical, and social) and address a 
range of challenges including vulnerability assessment, risk analysis, 
defense analysis, automated defensing, secure services composition, 
policy validation and verification. The objective of the GraMSec 
workshop is to contribute to the development of well-founded graphical 
security models, efficient algorithms for their analysis, as well as 
methodologies for their practical usage.


TOPICS
The workshop seeks submissions from academia, industry, and government 
presenting novel research on all theoretical and practical aspects of 
graphical models for security. The topics of the workshop include, but 
are not limited to:


• Graphical models for threat modeling and analysis
• Graphical models for risk analysis and management
• Graphical models for requirements analysis and management
• Textual and graphical representation for system, organizational, and 
business security
• Visual security modeling and analysis of socio-technical and 
cyber-physical systems

• Graphical security modeling for cyber situational awareness
• Graphical models supporting the security by design paradigm
• Methods for quantitative and qualitative analysis of graphical 
security models

• Formal semantics and verification of graphical security models
• Methods for (semi-)automatic generation of graphical security models
• Enhancement and/or optimization of existing graphical security models
• Scalable evaluation of graphical security models
• Evaluation algorithms for graphical security models
• Dynamic update of graphical security models
• Game theoretical approaches to graphical security modeling
• Attack trees, attack graphs and their variants
• Stochastic Petri nets, Markov chains, and Bayesian networks for security
• UML-based models and other graphical modeling approaches for security
• Software tools for graphical security modeling and analysis
• Case studies and experience reports on the use of graphical security 
modeling paradigm


INVITED SPEAKER
To be decided.

PAPER SUBMISSION
We solicit two types of submissions:
• Regular papers (up to 15 pages, excluding the bibliography and 
well-marked appendices)

describing original and unpublished work within the scope of the workshop.
• Short papers (up to 7 pages, excluding the bibliography and 
well-marked appendices)

describing original and unpublished work in progress.

The reviewers are not required to read the appendices, so the papers 
should be intelligible without them. All submissions must be prepared 
using the LNCS style:

http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0

Each paper will undergo a thorough review process. All accepted (regular 
and short) papers will be included in the workshop's post-proceedings. 
The GraMSec 2017 post-proceedings will be published in the Lecture Notes 
in Computer Science (LNCS) series of Springer. Submissions should be 
made using the GraMSec 2017 EasyChair web site: 
https://www.easychair.org/conferences/?conf=gramsec17


IMPORTANT DATES
• Submission deadline: Sunday, May 21, 2017
• Acceptance notification: Friday, July 7, 2017
• Workshop: Monday, August 21, 2017

GENERAL CHAIR
• Sjouke Mauw, University of Luxembourg, Luxembourg

PROGRAM CHAIRS
• Peng Liu, Pennsylvania State University, USA
• Ketil Stølen, SINTEF Digital and University of Oslo, Norway

PC MEMBERS
Mathieu Acher, University Rennes 1, Inria, France
Massimiliano Albanese, George Mason University, USA
Ludovic Apvrille, Télécom ParisTech, France
Thomas Bauereiss, DFKI, Germany
Kristian Beckers, Technical University of Munich, Germany   
Giampaolo Bella, University of Catania, Italy
Stefano Bistarelli, Università di Perugia, Italy
Marc Bouissou, EDF RD, France
Frédéric Cuppens, Télécom Bretagne, France
Nora Cuppens-Boulahia, Télécom Bretagne, France
Binbin Chen, Advanced Digital Sciences Center, Singapore
Hervé Debar, Télécom SudParis, France
Harley Eades, Augusta University, USA
Mathias Ekstedt, KTH - Royal Institute of Technology, Sweden 


Ulrik Franke, Swedish Institute of Computer Science - SICS, Sweden  
Frank Fransen, TNO, The Netherlands
Olga Gadyatskaya, University of Luxembourg, Luxembourg  
Paolo Giorgini, University of Trento, Italy
Dieter  Gollmann, Hamburg University of Technology, 

[TYPES/announce] Call for Participation: LogiCS/RiSE Summer School on Logic, AI and Verification [July 3 to 5]

2017-05-04 Thread Jens Katelaan

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

[Apologies in advance should you receive multiple copies of this mail.]

--
   Call for Participation

  LogiCS/RiSE Summer School on Logic, AI and Verification
   July 3 -- 5, 2017, TU Wien, Vienna, Austria

   http://forsyte.at/laive-summer-school-2017

--

The doctoral college Logical Methods in Computer Science (LogiCS,
http://logic-cs.at/phd/) and the Austrian Society for Rigorous Systems
Engineering (RiSE, http://arise.or.at/) will host a summer school on
Logic, Artificial Intelligence and Verification at TU Wien, Vienna,
Austria from July 3 to July 5.

The summer school targets master and doctoral students in Computer 
Science and Mathematics with a strong interest in Logic, Artificial 
Intelligence and Automated Verification. The event is open to all 
interested students.


The school will feature the following lectures:

* Johannes Fuernkranz (TU Darmstadt):
  Introduction to Machine Learning

* Cezary Kaliszyk (University of Innsbruck):
  Machine Learning in Theorem Proving

* Dan Olteanu (University of Oxford):
  From Joins to Aggregates to Optimization Problems

* Diego Calvanese and Marco Montali (Free University of Bolzano-Bozen):
  Verification of Data-Centric Systems

* Matteo Maffei (TU Wien):
  TBA

Register until May 31 to profit from the early registration fee of €70!

For more information and registration, see
http://forsyte.at/laive-summer-school-2017



[TYPES/announce] 1-2 Ph.D positions on Combining Formal Methods and Machine Learning (U. of Oslo), 9. June 2017

2017-05-04 Thread Martin Steffen
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]



   __

Up to 2  PH.D POSITIONS in Combining Formal Methods and
Machine Learning

deadline: 9. June 2017

Dept. of Computer Science, University of Oslo

https://www.jobbnorge.no/ledige-stillinger/stilling/137456/phd-research-fellow-combining-formal-methods-and-machine-learning-1-2-positions
   __


PhD Research Fellow , 1-2 positions


* Context


A position as PhD Research Fellow in Formal Modeling and Analysis is
available at the Department of Informatics, University of Oslo. The
fellowship will be for a period of 3 years with no compulsory work and with
possibility to extend to 4 years with 25 % compulsory work (teaching
responsibilities at the Department or innovation activities in the SIRIUS
Center). Starting date is as soon as possible.

* Job description

The position is funded by SIRIUS (Center for Scalable Data Access in the
Oil and Gas Domain), a new Center for Research-Driven Innovation (SFI) at
the University of Oslo. It constitutes a long-term research initiative,
funded by the Norwegian Research Council involving both academic research
teams (UiO, NTNU and Oxford University) as well as industrial partners
including operators (Statoil), service companies (Schlumberger and DNV GL)
and IT companies (e.g., Computas, Evry, IBM). The center has as its main
goal to develop novel technologies to improve our ability to extract and
exploit information from large data stores. The position is hosted at the
IFI SIRIUS center, the Execution Modeling and Analysis group, where we
research systematic model exploration techniques to predict the behavior of
software/system executions based on the analysis of models.

The main focus of this PhD project will be to develop and study new
model-based engineering techniques for context-dependent adaptive systems,
exploiting the interplay between systematic model exploration and machine
learning techniques. In context-dependent adaptive systems, system behavior
depends on some contextual information (e.g., data coming from sensors) and
the systems must adapt based on their interactions with the environment. We
are interested in investigating techniques that combine formal executable
modeling with reinforcement learning algorithms to calibrate models and
simulate system behavior where its performance improves over time. Demands
on analysis techniques to understand context-dependent adaptive systems are
increasing in many industrial areas, such as manufacturing, healthcare,
oil, and automotive industries. Through SIRIUS, the PhD student will
have the opportunity to collaborate with industry and to apply the
developed techniques on real industrial cases.

Applicants should submit a statement of research interests or a project
outline for the PhD project, but it is expected that the successful
candidate will ultimately define their project jointly with their
supervisors during the first two months of the fellowship.The application
letter should discuss at least one research topic of interest to the
candidate, including a brief reflection about the scientific issues
involved and the possible choice of theory and method(s). This statement of
research purpose should not exceed one page.

* Requirements


Applicants must hold a Master's degree or equivalent in a relevant field
such as computing/informatics/software engineering/machine learning. A
solid background in computing science or software engineering is required.
Good knowledge on algorithms, formal methods, machine learning, and
software development skills and experiences will be considered an advantage
when candidates are ranked.


Additional formal requirements (excepted documents, procedural questions,
etc.) as well as information concerning the university as workplace is
available via the link given above.


[TYPES/announce] PPDP 2017: Call For Papers (Abstract 12 May / Paper 19 May)

2017-05-04 Thread Brigitte Pientka
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]



CALL FOR PAPERS 

   19th International Symposium on
  Principles and Practice of Declarative Programming
  PPDP 2017

Namur, Belgium, October 9-11, 2017
  (co-located with LOPSTR'17)

 http://complogic.cs.mcgill.ca/ppdp2017
   


 SUBMISSION DEADLINE: 12 May (abstracts) / 19 May (papers)



PPDP  2017  is a  forum  that  brings  together researchers  from  the
declarative  programming communities, including  those working  in the
functional, logic, answer-set, and constraint programming
paradigms. The  goal is to stimulate research  in the use  of logical formalisms
and  methods for  analyzing, performing, specifying, and  reasoning about
computations, including mechanisms for concurrency, security, static
analysis, and verification. 

Submissions are invited on all topics from principles to practice,
from foundations to applications. Topics of interest include, but are
not limited to 

** Language Design: domain-specific languages; interoperability;
  concurrency, parallelism, and distribution; modules;
  probabilistic languages; reactive languages; database
  languages; knowledge representation languages; languages
  with objects; language extensions for tabulation;
  metaprogramming.

** Implementations: abstract machines; interpreters; compilation;
compile-time and run-time optimization; garbage collection; memory
management.

** Foundations: type systems; type classes; dependent types; logical
frameworks; monads; resource analysis; cost models;
continuations; control; state; effects; semantics.

** Analysis and Transformation: partial evaluation; abstract
 interpretation; control flow; data flow; information flow;
 termination analysis; resource analysis; type inference and
 type checking; verification; validation; debugging; testing.

** Tools and Applications: programming and proof
   environments; verification tools; case studies in proof assistants
   or interactive theorem provers; certification; novel applications
   of declarative programming inside and outside of CS;
   declarative programming pearls; practical experience reports
   and industrial application; education.

This year the conference will be co-located with the  27th Int'l Symp.  
on Logic-Based Program Synthesis and Transformation (LOPSTR 2017).

IMPORTANT DATES:

Abstract Submission:12 May   2017
Paper Submission:   19 May   2017
Paper Rebuttal: 10 July  2017
Notification:   20 July  2017
Final Version:  15 Aug   2017

SUBMISSION CATEGORIES:

Submissions can be made in three categories: regular Research Papers, 
System Descriptions, and Experience Reports.

Submissions of Research Papers must present original research which is
unpublished and not submitted elsewhere. They must not exceed 12 pages
ACM style 2-column (including figures and bibliography). Work that
already appeared in unpublished or informally  published workshop
proceedings may be submitted (please contact the PC chair in case of
questions). Submissions of research papers  will be judged on
originality, significance, correctness, clarity, and readability.

Submission of System Descriptions must describe a working system whose
description has not been published or submitted elsewhere. They must
not exceed 10 pages and should contain a link to a working system. System
Descriptions must be marked as such at the time of submission and will
be judged on originality, significance, usefulness, clarity, and readability. 

Submissions of Experience Reports are meant to
help create a body of published, refereed, citable evidence where
declarative programming such as functional, logic, answer-set,
constraint programming, etc., is used in practice. They must not
exceed 6 pages. Experience Reports must be marked as such at the time
of submission and need not report original research results.  They
will be judged on significance, usefulness, clarity, and readability.

Possible topics for an Experience Report include, but are not limited to:
  * insights gained from real-world projects using declarative
programming 
  * comparison of declarative programming with conventional
programming in the context of an industrial project or a
university curriculum 
  * curricular issues encountered when using declarative programming
in education 
  * real-world constraints that created special challenges for an
implementation of a declarative language or for declarative
programming in 

[TYPES/announce] Learning and Automata workshop: call for participation, early reg deadline 5 May

2017-05-04 Thread Sam Staton
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

CALL FOR PARTICIPATION
Learning and Automata (LearnAut) — LICS 2017 Workshop
June 19, Reykjavik (Iceland)
Early registration: May 5th (VERY SOON)
https://learnaut.wordpress.com/

Grammatical Inference studies machine learning algorithms for classical 
recursive models of computations like automata and grammars. The expressive 
power of these models and the complexity of associated computational problems 
are a major research topic within theoretical computer science. This workshop 
aims at offering a favorable place for dialogue and at generating discussions 
between researchers from these two communities.

The following papers have been accepted for oral presentation:

- Enes Avcu, Chihiro Shibata and Jeffrey Heinz: Subregular Complexity and Deep 
Learning
- Alexander Clark: Strong learning of Probabilistic Context-Free Grammars from 
Strings
- Nathanaël Fijalkow: Bisimulation on Distributions for Markov Decision 
Processes
- Oded Maler and Irini-Eleftheria Mens: On Learning Symbolic Automata over 
Boolean Alphabets
- Ariadna Quattoni, Xavier Carreras and Matthias Gallé. Scalable Spectral 
Learning of Automata through Maximum Matching
- Rick Smetsers: Grammatical Inference as a Satisfiability Modulo Theories 
Problem

In addition, the papers accepted for poster presentation are:

- Giovanni Bacci, Giorgio Bacci, Kim Guldstrand Larsen and Radu Mardare: On the 
Metric-based Approximate Minimization of Markov Chains
- Simone Barlocco and Clemens Kupke: Automata Learning: A Modal Logic 
Perspective
- Michael Bukatin and Jon Anthony: Dataflow Matrix Machines as a Model of 
Computations with Linear Streams
- Kaizaburo Chubachi, Diptarama, Ryo Yoshinaka and Ayumi Shinohara: Query 
Learning of Regular Languages over Large Ordered Alphabets
- Joshua Moerman: Learning Product Automata
- Tianyu Li, Guillaume Rabusseau and Doina Precup: Neural Network Based 
Nonlinear Weighted Finite Automata
- Alexis Linard, Rick Smetsers, Frits Vaandrager, Umar Waqas, Joost van Pinxten 
and Sicco Verwer: Learning Pairwise Disjoint Simple Languages from Positive 
Examples
- Xiaoran Liu, Qin Lin, Sicco Verwer and Dmitri Jarnikov: Anomaly Detection in 
a Digital Video Broadcasting System Using Timed Automata
- Guillaume Rabusseau and Joelle Pineau: Multitask Spectral Learning of 
Weighted Automata
- Michal Soucha and Kirill Bogdanov: Efficient Active Learning with Extra States

The following top researchers will be invited speakers at LearnAut:
- Kim G. Larsen (Aalborg University)
- Mehryar Mohri (New York University & Google Research)
- Alexandra Silva (University College London)

If you have not registered yet to the workshop, and if you are interested by 
its program, we strongly recommend you to do it as soon as possible 
(http://www.icetcs.ru.is/lics2017-registration.html). The early registration 
deadline is on May 5th.

Pressures on accommodation possibilities are high, the sooner you book one the 
better it is (a lot of hotels are unfortunately already full). 

Looking forward to seeing you at Reykjavik!

Borja Balle (Amazon)
Leonor Becerra-Bonache (Jean Monnet)
Remi Eyraud (Aix-Marseille)




[TYPES/announce] APLAS 2017: Asian Symposium on Programming Languages and Systems, CfP, June 13 deadline

2017-05-04 Thread Bor-Yuh Evan Chang
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

*
APLAS 2017 Call for Papers
15th Asian Symposium on Programming Languages and Systems

Suzhou, China, November 27-29, 2017

https://www-aplas.github.io/
*

# Important Dates

- Abstract deadline: Tuesday, June 13, 2017
- Paper deadline: Friday, June 16, 2017
- Author response: Wednesday-Friday, July 26-28, 2017
- Author notification: Monday, August 14, 2017
- Camera-ready deadline: Friday, September 1, 2017
- Conference: Monday-Wednesday, November 27-29, 2017

All deadline times are AoE.

# About

APLAS aims to stimulate programming language research by providing a forum
for the presentation of latest results and the exchange of ideas in
programming languages and systems. APLAS is based in Asia but is an
international forum that serves the worldwide programming languages
community.

APLAS is sponsored by the Asian Association for Foundation of Software
(AAFS), founded by Asian researchers in cooperation with many researchers
from Europe and the USA. Past APLAS symposiums were successfully held in
Hanoi ('16), Pohang ('15), Singapore ('14), Melbourne ('13), Kyoto ('12),
Kenting ('11), Shanghai ('10), Seoul ('09), Bangalore ('08), Singapore
('07), Sydney ('06), Tsukuba ('05), Taipei ('04), and Beijing ('03) after
three informal workshops. Proceedings of the past symposiums were published
in Springer's LNCS.

# Topics

The symposium is devoted to foundational and practical issues broadly
spanning the areas of programming languages and systems. Papers are
solicited on topics such as

- semantics, logics, foundational theory
- design of languages, type systems, and foundational calculi
- domain-specific languages
- compilers, interpreters, abstract machines
- program derivation, synthesis, and transformation
- program analysis, verification, model-checking
- logic, constraint, probabilistic, and quantum programming
- software security
- concurrency and parallelism
- tools and environments for programming and implementation

Topics are not limited to those discussed in previous symposiums. Papers
identifying future directions of programming and those addressing the rapid
changes of the underlying computing platforms are especially welcome.
Demonstration of systems and tools in the scope of APLAS are welcome to the
System and Tool demonstrations category. Authors concerned about the
appropriateness of a topic are welcome to consult with program chair prior
to submission.

# Submission

We solicit submissions in two categories:

- **Regular research papers** describing original scientific research
results, including system development and case studies. Regular research
papers *should not exceed 18 pages* in the Springer LNCS format, including
bibliography and figures.  This category encompasses both theoretical and
implementation (also known as system descriptions) papers.  In either case,
submissions should clearly identify what has been accomplished and why it
is significant.  Submissions will be judged on the basis of significance,
relevance, correctness, originality, and clarity.  System descriptions
papers should contain a link to a working system and will be judged on
originality, usefulness, and design.  In case of lack of space, proofs,
experimental results, or any information supporting the technical results
of the paper could be provided as an appendix or a link to a web page, but
reviewers are not obliged to read them.

- **System and tool demonstrations** describing a demonstration of a tool
or a system that support theory, program construction, reasoning, or
program execution in the scope of APLAS. The main purpose of a tool paper
is to display a completed, robust and well-documented tool--highlighting
the overall functionality of the tool, the interfaces of the tool,
interesting examples and applications of the tool, an assessment of the
tool's strengths and weaknesses, and a summary of documentation/support
available with the tool. Authors of tool demonstration proposals are
expected to present a live demonstration of the tool at the conference. It
is highly desirable that the tools are available on the web. System and
Tool papers should not exceed 8 pages in the Springer LNCS format,
including bibliography and figures. They may include an additional appendix
of up to 6 extra pages giving the outline, screenshots, examples, etc. to
indicate the content of the proposed live demo.

Papers should be submitted electronically via the submission web page
https://easychair.org/conferences/?conf=aplas2017 using EasyChair. The
acceptable format is PDF.

Submitted papers must be unpublished and not submitted for publication
elsewhere. Papers must be written in English. The proceedings will be
published as a volume in Springer's LNCS series. Accepted papers must be

[TYPES/announce] PhD position on Security and Privacy of Location-Based Services at at Chalmers

2017-05-04 Thread Andrei Sabelfeld

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



PhD position on Security and Privacy of Location-Based Services at Chalmers 
University of Technology, Sweden

Application deadline: May 31, 2017


*Job description*

The Department of Computer Science and Engineering at Chalmers University of 
Technology invites applications for a PhD position in Security and Privacy of 
Location-Based Services.

The PhD student will join a world-leading team of researchers on software 
security and privacy. Software is often the root cause of vulnerabilities in 
modern computing systems. By focusing on securing the software, we target 
principled security mechanisms that provide robust protection against large 
classes of attacks.

The advertised position is on Security and Privacy of Location-Based Services. 
The position is a part of Wallenberg Autonomous Systems and Software Program 
(WASP), Sweden's largest individual engineering research program.

Location-based services/systems (LBS) see tremendous growth, with application 
from smartphones to autonomous vehicles and aircraft. This project is on 
rigorous techniques for security and privacy in LBS, including:

-security and privacy foundations of LBS: formal modeling and reasoning for LBS 
policies;

-application-, service-, and system-level mechanisms: enforcing security and 
privacy policies for LBS by such software-level techniques as informationflow 
control (IFC), program analysis, and monitoring, and their integration with 
such hardware-level mechanisms as Isolated Execution Environments (IEE) and 
infrastructure for secure localization;

-cryptographic techniques for LBS: designing and scaling decentralized 
approaches, such as those enabled by secure multi-party computation.

This position will be supervised by Prof. Andrei Sabelfeld 
http://www.cse.chalmers.se/~andrei/


*Details about employment*

PhD student position is limited to five years and normally include 20 per cent 
departmental work, mostly teaching duties. Salary for the position is as 
specified in Chalmers' general agreement for PhD student positions. Currently 
the starting salary is around 30,000SEK a month before tax.  The position is 
intended to start in fall 2017.


*Suitable background*

Applicants should have a Master's Degree or corresponding degree in Computer 
Science, Computer Engineering, or in a related discipline.  As for all PhD 
studies, a genuine interest and curiosity in the subject matter and excellent 
analytical and communication skills, both oral and written, are needed.

You may apply even if you have not completed your degree, but expect to do so 
before the position starts.  Knowledge of Swedish is not a prerequisite for 
applying since English is our working language for research, and we publish 
internationally.  Both Swedish and English are used in undergraduate courses.  
Half of our researchers and PhD students at the department come from more than 
30 different countries.


*How to apply*

The application should be submitted electronically via the following link:

http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job=5052


*The department*

The department has about 260 employees from more than 30 countries. The 
research spans the whole spectrum, from theoretical foundations to applied 
systems development. There is extensive national and international 
collaboration with academia and industry all around the world. For more 
information, see http://www.chalmers.se/en/departments/cse/Pages/default.aspx


*Gothenburg, Sweden*

Gothenburg is often referred to as the "heart of Scandinavia".

"This is Gothenburg" video: https://www.youtube.com/watch?v=QkCgd9YfZ34


[TYPES/announce] PhD and Postdoc positions in Innsbruck

2017-05-04 Thread Cezary Kaliszyk
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We invite candidates for multiple PhD student and Postdoc researcher
positions to start in 2017 or 2018 in the 5-year project
"Strong Modular Proof Assistance: Reasoning across Theories" in the
CL group at the University of Innsbruck.

The starting date can be negotiated. PhD student positions like Postdoc
positions are formal employment in Austria, with a regular salary and
benefits. Applications before June 15 will receive a full consideration.

A background in proof assistants or machine learning is an advantage.
Knowledge of German is not required, the group is international and
the language of communication is English.

Candidates for a PhD position must hold a MSc in computer science or
mathematics and candidates for the postdoctoral position hold a PhD
degree in computer science or mathematics.

Applications and informal inquiries are welcome, please contact
Cezary Kaliszyk (cezary.kalis...@uibk.ac.at). Applications should
include a CV and names and contact details of two references.
For the Postdoc positions please include a brief research statement.

The city of Innsbruck, which hosted the Olympic Winter Games in 1964,
1976 and 2012 (YOG), is superbly located in the beautiful surroundings
of the Tyrolean Alps. The combination of the Alpine environment and
urban life in this historic town provides a high quality of living.
The CL group is one of the leading groups concerned with formalization
and certification in the world.

More information and links about the project, the group, and the university:

http://cl-informatik.uibk.ac.at/cek/smart/


-- 
Cezary Kaliszyk, University of Innsbruck,
http://cl-informatik.uibk.ac.at/cek/


[TYPES/announce] 2nd CFP: Workshop on Type-driven Development (TyDe '17)

2017-05-04 Thread Sam Lindley

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


CALL FOR PAPERS

2nd Workshop on Type-Driven Development (TyDe '17)
 3 September 2017, Oxford, UK

 http://tydeworkshop.org/2017


# Goals of the workshop

The workshop on Type-Driven Development aims to show how static type
information may be used effectively in the development of computer
programs. Co-located with ICFP, this workshop brings together leading
researchers and practitioners who are using or exploring types as a
means of program development.

We welcome all contributions, both theoretical and practical, on a
range of topics including:

-   dependently typed programming;
-   generic programming;
-   design and implementation of programming languages, exploiting types
in novel ways;
-   exploiting typed data, data dependent data, or type providers;
-   static and dynamic analyses of typed programs;
-   tools, IDEs, or testing tools exploiting type information;
-   pearls, being elegant, instructive examples of types used in the
derivation, calculation, or construction of programs.

# Invited speaker

Andrew Kennedy, Facebook, UK

# Program Committee

-   Nada Amin, EPFL, Switzerland
-   Ana Bove, Chalmers University of Technology, Sweden
-   Patricia Johann, Appalachian State University, US
-   Yukiyoshi Kameyama, University of Tsukuba, Japan
-   Sam Lindley, The University of Edinburgh, UK (co-chair)
-   Limin Jia, CMU, US
-   Assia Mahboubi, INRIA Saclay, France
-   Liam O’Connor, University of New South Wales, Australia
-   Nicolas Oury, Jane Street, UK
-   Jennifer Paykin, University of Pennsylvania, US
-   Paula Severi, University of Leicester, UK
-   Tarmo Uustalu, Tallinn University of Technology, Estonia
-   Jeremy Yallop, University of Cambridge, UK
-   Brent Yorgey, Hendrix College, US (co-chair)

# Proceedings and Copyright

We plan to have formal proceedings, published by the ACM. Accepted
papers will be included in the ACM Digital Library. Authors must grant
ACM publication rights upon acceptance, but may retain copyright if they
wish. Authors are encouraged to publish auxiliary material with their
paper (source code, test data, and so forth). The proceedings will be
freely available for download from the ACM Digital Library from one week
before the start of the conference until two weeks after the conference.

# Submission details

Submissions should fall into one of two categories:

-   Regular research papers (12 pages)
-   Extended abstracts (2 pages)

The bibliography will not be counted against the page limits for
either category.

Regular research papers are expected to present novel and interesting
research results, and will be included in the formal
proceedings. Extended abstracts should report work in progress that
the authors would like to present at the workshop. Extended abstracts
will be distributed to workshop attendees but will not be published in
the formal proceedings.

We welcome submissions from PC members (with the exception of the two
co-chairs), but these submissions will be held to a higher standard.

Submission is handled through HotCRP:

  https://icfp-tyde17.hotcrp.com/

All submissions should be in portable document format (PDF) and
formatted using the ACM SIGPLAN style guidelines:

  http://www.sigplan.org/Resources/Author/

*Note* that the ACM SIGPLAN style guidelines have changed from
previous years! In particular, submissions should use the new
‘acmart’ format and the two-column ‘sigplan’ subformat (not to be
confused with the one-column ‘acmlarge’ subformat!).

Extended abstracts must be submitted with the label 'Extended
abstract' clearly in the title.

# Important Dates

-   Regular paper deadline: Wednesday, 24th May, 2017
-   Extended abstract deadline: Wednesday, 7th June, 2017
-   Author notification: Wednesday, 28th June, 2017
-   Deadline for camera ready version: Saturday, 15th July, 2017
-   Workshop: Sunday, 3rd September, 2017

# Travel Support

Student attendees with accepted papers can apply for a SIGPLAN PAC grant
to help cover travel expenses. PAC also offers other support, such as
for child-care expenses during the meeting or for travel costs for
companions of SIGPLAN members with physical disabilities, as well as for
travel from locations outside of North America and Europe. For details
on the PAC program, see its web page:

  http://www.sigplan.org/PAC/

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