[TYPES/announce] Final Announcement: Second DeepSpec Summer School

[Lennart Beringer]

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

[Application deadline: March 23rd]

 Second DeepSpec Summer School (DSSS'18)
 Princeton, NJ, July 16-27, 2018
https://deepspec.org/event/dsss18
  
Overview

Can critical systems be built according to functionally precise
specifications of of their constituent components (processor,
operating system, crypto library,..) and development tools (compilers,
synthesis tools)? This may seem a pipe dream, but the past decade has
seen remarkable advances in the technology required to realize it. The
DeepSpec summer school will provide students with knowledge and
experience necessary for understanding the state of the art and for
contributing to ongoing research efforts, based on the interactive
proof assistant Coq. The school is supported by generous funding from
the National Science Foundation.

DSSS'18 will consist of two parts with the first week being devoted to
introductory topics and the second week covering current research
efforts.

July 16-18 (Mon-Wed) Coq Intensive
July 19-20 (Thu-Fri) Fundamental proof techniques and project overviews
July 23-27 (week 2)  Advanced topics in system verification

Lecturers and Topics for week 2
---
Andrew Appel and Verifiable C: a logic and toolset for
Lennart Beringer proving C programs correct

Adam ChlipalaImplementing, specifying, verifying,
 and compiling hardware components with Kami 

Zach Tatlock Verifying distributed systems

Benjamin Pierce  Property-based random testing with QuickChick

All DeepSpec PIs Towards the specification and verification of a
 web server

Prerequisites
-
DSSS'18 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 familiar with Coq at the level of
Software Foundations (Volume 1) should plan on attending the Coq
Intensive. Participants unfamiliar with volumes 2 and 3 may benefit
from attending the last 3 days of week 1.

Participants of DSSS'17 are likely to be admitted for participation in
week 2 only.  

Application and participation
-
Participation in DSSS'18 is by invitation only, based on an
application process that is open to anybody. To apply, please fill
this application form

https://www.regonline.com/builder/site/?eventid=2209458

preferably no later than March 23, 2018. Accepted participants will be
notified shortly thereafter, and will be invited to confirm their
participation by registering.

Thanks to the generosity of NSF, we will be able to provide
substantial financial assistance to all participants. We will not
charge a registration fee, and will offer free dorm accommodation on
the campus of Princeton University. In addition, we expect to
subsidize travel expenses for the majority of participants, based on
their geographic origin, qualification, and financial needs. To help
us allocating these funds, the application form includes the option to
enter estimated travel costs etc..

Late applications will be handled on a case-by-case basis.  

For additional information on the DeepSpec project, please see
https://deepspec.org.

[TYPES/announce] 4PAD 2018 (deadline extension): 5th International Symposium on Formal Approaches to Parallel and Distributed Systems

[Frederic Loulergue]

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

*** Apologies if you receive multiple copies. ***

*** Please forward to interested colleagues.  ***

Extended deadline : April 8th, 2018




=    CALL FOR PAPERS   =
= 5th International Symposium on   =
=   Formal Approaches to Parallel and Distributed Systems  =
=  (4PAD 2018) =
=  affiliated to the   =
=  16th International Conference on    =
=  High Performance Computing & Simulation (HPCS 2018) =
= http://hpcs2018.cisedu.info/ =
= Orleans, France, July 17-19, 2018    =


http://hpcs2018.cisedu.info/2-conference/symposia---hpcs2018/symp05-4pad

SCOPE AND OBJECTIVES

The aim of 4PAD is to foster interaction between the formal methods
communities and systems researchers working on topics in modern
parallel, distributed, and network-based processing systems (e.g.,
autonomous computing systems, cloud computing systems,
service-oriented systems and parallel computing architectures).

4PAD topics include (but are not limited to) the following:

* Rigorous software engineering approaches and their tool support;
* Model-based approaches, including model-driven development;
* Service- and component-based approaches;
* Semantics, types and logics;
* Formal specification and verification;
* Performance analysis based on formal approaches;
* Formal aspects of programming paradigms and languages;
* Formal approaches to parallel architectures and weak memory models;
* Formal approaches to deployment, run-time analysis,
  adaptation/evolution, reconfiguration, and monitoring;
* Case studies developed/analyzed with formal approaches;
* Formal stochastic models and analysis;
* Formal methods for large-scale distributed systems;
* Statistical analysis techniques based on formal approaches.

PAPER SUBMISSION AND PUBLICATION

You are invited to submit original and unpublished research works on
above and other topics related to Formal Approaches to Parallel and
Distributed Systems.  Submitted papers must not have been published or
simultaneously submitted elsewhere until it appears in HPCS
proceedings, in the case of acceptance, or notified otherwise. For
Regular papers, please submit a PDF copy of your full manuscript, not
to exceed 8 double-column IEEE formatted pages per template, and
include up to 6 keywords and an abstract of no more than 400 words.
Short papers (up to 4 pages), poster papers and posters (please refer
to
http://hpcs2018.cisedu.info/1-call-for-papers-and-participation/call-for-posters
for posters submission details) will also be considered. Please
specify the type of submission you have.  Please include page numbers
on all preliminary submissions to make it easier for reviewers to
provide helpful comments.

Submit a PDF copy of your full manuscript to the symposium paper
submission site at https://easychair.org/conferences/?conf=4pad.

IMPORTANT DATES

Paper Submissions: April 8, 2018 (extended, firm)
Acceptance Notification: April 26, 2018
Camera Ready Papers and Registration Due by: May 11, 2018
Conference Dates (HPCS and affiliated events): July 16-20, 2018

SPECIAL ISSUE

After the symposium, authors of selected papers will be invited to
submitted extended version of their papers for possible publication in
a special issue of the Journal of Logical and Algebraic Methods in
Programming (JLAMP).

PROGRAM COMMITTEE

Gul Agha        University of Illinois at Urbana-Champaign, USA
Marco Aldinucci        University of Torino, IT
Allan Blanchard        Inria, FR
Simon Bliudze        Inria, FR
Laura Bocchi        University of Kent, UK
Jean-Michel Couvreur     University of Orleans, FR, chair
Kento Emoto        Kyushu Institute of Technology, JP
Gidon Ernst        National Institute of Informatics, JP
Joaquin Ezpeleta    Universidad de Zaragoza, ES
Ylies Falcone        Univ. Grenoble Alpes, Inria, FR
Serge Haddad        LSV, ENS Cachan, CNRS, Inria, FR
Ludovic Henrio        CNRS, FR
Claude Jard        University of Nantes, FR
Igor Konnov        Vienna University of Technology, AT
Sandeep Kulkarni    Michigan State University, USA
Alberto Lluch Lafuente    Technical University of Denmark, DK
Frederic Loulergue     Northern Arizona University, USA, chair
Neeraj Mittal        The University of Texas at Dallas, USA
Gwen Salaun        University of Grenoble Alpes, FR
Sven Schewe        University of Liverpool, UK
Elena Sherman        Boise State University,    USA
Francesco Tiezzi    Universita di Camerino, IT
Enrico    Tronci        Sapienza University of Rome, IT
Emilio Tuosto        University of Leicester, UK

[TYPES/announce] Postdoc position in Orsay, France

[Sylvie Boldo]

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

Hello,

I would like to advertise a postdoc position available in Orsay, France.
The goal is to develop formal proofs about the floating-point evaluation of 
polynomials and is within the FastRelax project

  http://fastrelax.gforge.inria.fr/


To see details and to apply, please go to
  https://jobs.inria.fr/public/classic/en/offres/2018-00418

Do not hesitate to forward this email to any appropriate candidate or
mailing list.

Best regards,

Sylvie Boldo

--
Sylvie Boldo, Toccata project, Inria Saclay - Île-de-France
PCRI, Bât. 650 - Université Paris-Sud - 91405 ORSAY Cedex

[TYPES/announce] SAT/SMT/AR Summer School 2018

[Giles Reger]

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

[Apologise for cross-posting. Please forward to anybody you think may be 
interested]


SAT/SMT/AR Summer School 2018
University of Manchester, 3-6th July
http://ssa-school-2018.cs.manchester.ac.uk


We are pleased to announce that the next edition of the SAT/SMT/AR Summer
School will take place in Manchester, UK on 3-6th July 2018. Satisfiability
(SAT), Satisfiability Modulo Theories (SMT), and Automated Reasoning (AR)
continue to make rapid advances and find novel uses in a wide variety of
applications, both in computer science and beyond.

The SAT/SMT/AR Summer School aims to bring a select group of students up to
speed quickly in this exciting research area. The school continues the
successful line of Summer Schools that ran from 2011 to 2015 as SAT/SMT Summer
Schools and added AR in 2016. There will also be a special session on computer
algebra to continue the activity of the SC2 summer school in 2017.

Lecturers for this year's summer school have been announced on the school's
website and detailed programme of topics will appear soon.

http://ssa-school-2018.cs.manchester.ac.uk/index.php/speakers/

Applications can be made via the following form

https://goo.gl/forms/e2hgn5GbnPROMTEK2

Registration is £100 for applicants before 1st April and may raise to £200 
after this
date (subject to level of interest). Grants for registration fee reduction and 
to (partially)
cover accommodation costs are available and should be applied for with the above
form. Grants will be awarded based on need but those applying earlier (in 
particular,
before the 1st April) will be prioritised. Note that we have separate 
application and
registration phases and these dates apply to application rather than 
registration.

Important Dates
=
Early Registration 1st April
Registration Closes 1st May
Summer School 3-6th July

Organisers
=
Giles Reger, University of Manchester
Konstantin Korovin, University of Manchester
Andrew Reynolds, University of Iowa

[TYPES/announce] Visiting PhD Student

[Harley D. Eades III]

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

Are you or do you know a PhD student looking for an exciting new
funded research project to join this summer or fall?  You are in luck!

I am looking for a visiting PhD student for summer or fall 2018 to
collaborate with me on a funded NSF project working in the
intersection of graphical models of security, functional programming
using category theory, linear logic, and dependent types for
substructrual logics.

This opporunity comes with a $5,000 stipend to cover food and lodging
during the visit.  I have additional money to pay for your travel.

There are two ongoing projects the student can join depending on their
interests. Both of these projects have lots of exciting problems to
solve.

=Project 1=

CRII: SHF: A New Foundation for Attack Trees Based on Monoidal Categories

In short, the project aims to give a new mathematical foundation of
attack trees using monoidal categories, and then by capitalizing on
the Curry-Howard-Lambek correspondence, defining a new domain-specific
functional programming language based in linear logic where types will
correspond to attack trees, and programs to semantically valid
transformations on attack trees called Lina for Linear Threat
Analysis.

More information on the project including the complete proposal can be
found here:

https://github.com/MonoidalAttackTrees

The Lina language is under active developement, you can find the
language here:

https://github.com/MonoidalAttackTrees/Lina

=Project 2=

In collaboration with Dominc Orchard
(https://www.cs.kent.ac.uk/people/staff/dao7/), and his student Vilem
Liepelt, at the University of Kent, we are working on a new linear
dependent type theory based on graded modal type theory.

Using graded coeffects our language allows the programmer to control
various structural rules with minimal annotations, thus, producing a
very elegant and general framework with full dependency for various
substructural logics.

This project can also be seen as a generalization of the Granule
language, please find more info here:

https://github.com/dorchard/granule

We are just getting started, but we do have some initial results.

The interested student would help with the specification of our
new type theory, as well as, exploring categorical models, and/or
even implementation of the language prototype.

=Who I am looking for?=

I am looking for an energetic and passionate student to work closely
with me on one of the above projects during the summer or fall of
2018.  The visit will be three months in total, but specific dates
will be discussed with each candidate.

The hope is for the student and I to work towards some results that
can be published during the following academic year.

The student should have an interest, but does not have to be
experienced, in some of the following topics:

- Models of security,
- Categorical logic,
- Intuitionistic linear logic,
- Dependent type theory, or
- The design and anlysis of statically-typed functional programming
  languages.

Experience in category theory is a plus, but not strictly required as
long as the student is willing to learn.

=Who am I?=

I am an assistant professor in computer science at Augusta University
in the wonderful Augusta Georgia.  More about me here:

http://metatheorem.org/

Augusta is perfectly positioned on the border of Georiga and South
Carolina only two and a half hours from Savannah, GA and the beach at
Tybee Island.  In addition, we are only three hours away from the
Great Smokey Mountains for those who enjoy the great outdoors.

=How to apply?=

Simply send me an email with your CV and a brief summary of your
research interests.  I will be considering applications until April
20th.

I welcome emails from anyone who is interested!

This is an equal opportunity for all! All interested applicants will
receive consideration without regard to race, color, religion, sex,
national origin, disability status, protected veteran status, or any
other characteristic protected by law.

Very best,
Harley Eades

[TYPES/announce] Call for papers : HOR 18 - 9th Workshop on Higher Order Rewriting, Oxford, 7 July, 2018

[Stefano Guerrini]

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

--
--
**
**HOR 18
**9th Workshop on Higher-Order Rewriting
**
**http://lipn.univ-paris13.fr/HOR18
**
--
**
**International Workshop affiliated with FSCD at FLOC 2018
**http://www.cs.le.ac.uk/events/fscd2018
**http://floc2018.org
**
**Oxford, 7 July, 2018
**
--
**
**Call for Submissions 
**http://lipn.univ-paris13.fr/HOR18/call-for-submissions.txt
**
--
--

* Overview

HOR is a forum to present work concerning all aspects of higher-order
rewriting.

HOR aims to provide an informal and friendly setting to discuss recent
work and work in progress concerning higher-order rewriting, broadly
construed. This includes rewriting systems that have functional
variables or bound variables, the lambda-calculus and combinatory
logic being paradigmatic examples.

* Topics

The following is a non-exhaustive list of topics for the workshop:

  - Applications: proof checking, theorem proving, generic
programming, declarative programming, program transformation.

  - Foundations: pattern matching, unification, strategies, narrowing,
termination, syntactic properties, type theory.

  - Frameworks: term rewriting, conditional rewriting, graph
rewriting, net rewriting, comparisons of different frameworks.

  - Implementation: graphs, nets, abstract machines, explicit
substitution, rewriting tools, compilation techniques.

  - Semantics: operational semantics, denotational semantics,
separability, higher-order abstract syntax.

--
** Submission Guidelines
--

To give a presentation at the workshop, submit an extended asbtract
(between 2 to 5 pages} via Easychair

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

HOR is a platform for discussing open questions, ongoing research, and
new perspectives, as well as new results. Extended abstracts
describing work in progress, preliminary results, reserch projects, or
problems in higher-order rewriting are very welcome.

The workshop has informal, electronic proceedings that will be
included in the FLoC 2018 electronic proceedings.

Submission is via Easychair at

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

For questions regarding submission, please contact the PC chair
  Stefano Guerrini  (mailto:stefano.guerr...@univ-paris13.fr)

--
** Important dates
--

 * Submission deadline: 15 April, 2017
 * Notification: 22 May, 2017
 * Final version: 28 May, 2017

--
** Committees
--

** Program Committee
--

 * Sandra Alves(University of Porto, Portugal)
 * Zena Ariola(University of Oregon, Oregon, USA)
 * Eduardo Bonelli(Stevens Institute of Technology, New Jersey, USA)
 * Jörg Endrullis(Vrije Universiteit Amsterdam, The Netherlands)
 * Stefano Guerrini, chair(Paris 13 University, France)
 * Benedetto Intrigila(Tor Vergata University, Rome, Italy)
 * Paula Severi(University of Leicester, UK)
 * Femke Van Raamsdonk(Vrije Universiteit Amsterdam, The Netherlands)

** Steering Committee
--

 * Delia Kesner(IRIF, Univ. Paris Diderot)
 * Femke Van Raamsdonk(Vrije Universiteit Amsterdam, The Netherlands)

--
** Invited Speakers
--

 * TBA
 * TBA

--
** Contact
--

All questions about submissions should be emailed to
Stefano Guerrini (mailto:stefano.guerr...@univ-paris13.fr)

--
** Supporting Organisations
--

Université Paris 13, Sorbonne Paris Cité

=

Stefano Guerrini
Institut Galilée, Université Paris 13, Sorbonne Paris Cité
Laboratoire d'Informatique de Paris-Nord (LIPN), 

[TYPES/announce] LAP 2018 - Logic and Applications: CFP

[Silvia Ghilezan]

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

=
[ Please broadcast/post/forward. Apologies for duplicates]

LAP 2018 CONFERENCE ANNOUNCEMENT

LOGIC AND APPLICATIONS - LAP 2018
September 24-28, 2018, Dubrovnik, Croatia

http://imft.ftn.uns.ac.rs/math/cms/LAP2018 


The conference brings together researchers from various fields of logic with 
applications in computer science.
Topics of interest include, but are not restricted to:
- Formal systems of classical and non-classical logic;
- Category theory;
- Proof theory;
- Lambda calculus;
- Set theory;
- Type theory;
- Process algebras and calculi;
- Behavioural types;
- Systems of reasoning in the presence of incomplete, imprecise and/or 
contradictory information;
- Computational complexity;
- Interactive theorem provers;
- Security.

Student sessions will be organised.

Co-located event FORMALS 2018 http://formals.ufzg.hr/ 

LAP is a series of conferences held at IUC - Inter University Center Dubrovnik, 
Croatia.
The first conference Proof Systems was held on June 28, 2012, co-located with 
the conference LICS 2012, followed by 
LAP 2013, September 16-20, 2013 (http://imft.ftn.uns.ac.rs/math/cms/LAP2013 
)
LAP 2014, September 22-26, 2014 (http://imft.ftn.uns.ac.rs/math/cms/LAP2014 
)
LAP 2015, September 21-25, 2015 (http://imft.ftn.uns.ac.rs/math/cms/LAP2015 
)
LAP 2016, September 19-23, 2016 (http://imft.ftn.uns.ac.rs/math/cms/LAP2016 
)
LAP 2016, September 18-22, 2017 (http://imft.ftn.uns.ac.rs/math/cms/LAP2017 
)

IMPORTANT DATES
Abstract Submission: June 1, 2018
Author Notification: June 26, 2018
Final version: July 6, 2018

SUBMISSION
Authors should submit an abstract in LaTeX format, not exceeding three pages, to
v...@mi.sanu.ac.rs 
(with the subject "LAP 2018").

LOCATION:
IUC - Inter University Center Dubrovnik
http://www.iuc.hr/ 

COURSE DIRECTORS
- Zvonimir Šikić, University of Zagreb
- Andre Scedrov, University of Pennsylvania
- Silvia Ghilezan, University of Novi Sad
- Zoran Ognjanović, Mathematical Institute SANU, Belgrade
- Thomas Studer, University of Bern

==