[Hol-info] PhD studentship on the CakeML project (University of Kent)

[Scott Owens]

I am looking for a PhD student to work with me on the CakeML project at the
University of Kent in Canterbury, England. The position is part of the
"Building Verified Applications in CakeML" project funded by the UK Research
Institute in Verified Trustworthy Software Systems:
https://vetss.org.uk/funded-proposals/.

CakeML (https://cakeml.org) is a formally verified compiler for an ML-like
programming language. The studentship is focussed on techniques for formally
verifying applications written in the CakeML language. Within the project,
there is a wide range of possible topics, ranging from fully automated
verification to techniques requiring interactive proof, and also from the logic
and mathematics that underpin verification to the creation of a practical
verification tool chain.

The student will be studying in the University of Kent's programming languages
research group which has 13 faculty members, and has notable strengths in
verification, concurrency, and functional programming. He or she will also work
with the broader international CakeML community at Chalmers (Sweden), CMU
(USA), and Data61 (Australia).

The position starts in September 2018. Applicants must have, or be about to
complete a degree in Computer Science or Mathematics at the BSc or MSc level.
The position is fully funded for 3.5 years for students from the UK/EU.

Interested candidates should contact me by 21 May, 2018.

Scott Owens
http://www.cs.kent.ac.uk/~sao


--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] WADT 2018 - Extension to abstract submission deadline!

[WADT 2018]

==
FOURTH CALL FOR PAPERS - Extension to abstract submission deadline!

WADT 2018
24th International Workshop on Algebraic Development Techniques
http://wadt18.cs.rhul.ac.uk
July 2–5, 2018, Royal Holloway University of London, Egham, UK
==

AIMS AND SCOPE

The algebraic approach to system specification encompasses many aspects of the 
formal design of software systems. Originally born as a formal method for 
reasoning about abstract data types, it now covers new specification frameworks 
and programming paradigms (such as object-oriented, aspect-oriented, 
agent-oriented, logic and higher-order functional programming) as well as a 
wide range of application areas (including information systems, concurrent, 
distributed and mobile systems). The workshop will provide an opportunity to 
present recent and ongoing work, to meet colleagues, and to discuss new ideas 
and future trends.

TOPICS OF INTEREST

Typical, but not exclusive topics of interest are:
– Foundations of algebraic specification
– Other approaches to formal specification, including process calculi and 
models of concurrent, distributed, and cyber-physical systems
– Specification languages, methods, and environments
– Semantics of conceptual modelling methods and techniques
– Model-driven development
– Graph transformations, term rewriting, and proof systems
– Integration of formal specification techniques
– Formal testing and quality assurance, validation, and verification
– Algebraic approaches to cognitive sciences, including computational creativity

WORKSHOP FORMAT AND LOCATION

The workshop will take place over four days, Monday to Thursday, at Royal 
Holloway University of London in Egham, UK (https://www.royalholloway.ac.uk).
Presentations will be selected on the basis of submitted abstracts.

This occurrence of the ADT workshop will be preceded by the Leverhulme School 
on Graph Transformation Techniques. The school will take place over three days, 
from Friday, June 29th, to Sunday, July 1st, and will comprise a self-contained 
series of invited lectures on graph transformation to be given by Reiko Heckel 
(University of Leicester, UK), Fernando Orejas (Technical University of 
Catalonia, Spain), and Detlef Plump (University of York, UK).

INVITED SPEAKERS

Artur d'Avila Garcez (City, University of London, UK)
Rolf Hennicker (LMU Munich, Germany)
Kai-Uwe Kühnberger (Osnabrück University, Germany)
Fernando Orejas (Technical University of Catalonia, Spain)

IMPORTANT DATES

Submission deadline for abstracts: May 11th, 2018
Notification of acceptance: May 25th, 2018
Early registration: June 1st, 2018
Final abstract due: June 8th, 2018
Leverhulme School on Graph Transformation Techniques: June 29–July 1, 2018
ADT Workshop: July 2–5, 2018

SUBMISSIONS

The scientific programme of the workshop will include presentations of recent 
results or ongoing research as well as invited talks. The presentations will be 
selected by the Steering Committee on the basis of submitted abstracts 
according to originality, significance and general interest. Abstracts must not 
exceed two pages including references; if a longer version of the contribution 
is available, it can be made accessible on the web and referenced in the 
abstract.

Abstracts have to be submitted electronically via the EasyChair system at 
https://easychair.org/conferences/?conf=wadt18.

PROCEEDINGS

After the workshop, authors will be invited to submit full papers for the 
refereed proceedings. All submissions will be reviewed by the Programme 
Committee. Selection will be based on originality, soundness, and significance 
of the presented ideas and results. The proceedings will be published as a 
volume of Lecture Notes in Computer Science (Springer).

The deadline for submissions will be September 3, 2018, with notifications by 
October 29. Camera-ready versions will be required by November 11.

SPONSORSHIP

The workshop takes place under the auspices of IFIP WG 1.3, while the series of 
graph-transformation lectures is supported by a Leverhulme Trust Visiting 
Professorship.

WADT STEERING COMMITTEE

Andrea Corradini (Italy)
José Fiadeiro (UK) [co-chair]
Rolf Hennicker (Germany)
Hans-Jörg Kreowski (Germany)
Till Mossakowski (Germany)
Fernando Orejas (Spain)
Markus Roggenbach (UK)
Grigore Roșu (United States)

PROGRAMME COMMITEE

Paolo Baldan (Italy)
Andrea Corradini (Italy)
Artur d'Avila Garcez (UK)
Răzvan Diaconescu (Romania)
José Fiadeiro (UK) [co-chair]
Fabio Gadducci (Italy)
Reiko Heckel (UK)
Rolf Hennicker (Germany)
Alexander Knapp (Germany)
Barbara König (Germany)
Antónia Lopes (Portugal)
Narciso Marti-Oliet (Spain)
Till Mossakowski (Germany)
Fernando Orejas (Spain)
Leila Ribeiro (Brazil)
Markus Roggenbach (UK)
Pierre-Yves Schobbens (Belgium)
Lutz Schröder (Germany)
Pawel Sobocinski (UK)
Ionuț Țuțu (UK) [co-chair]
Martin Wirsing (Germany)

[Hol-info] WST 2018 - Last Call for Papers (deadline: April 30, 2018)

[Salvador Lucas]

==
  WST 2018 - Call for Papers
   16th International Workshop on Termination

    July 18-19, 2018, Oxford, United Kingdom
  http://wst2018.webs.upv.es/

==

NEW: James Worrell and Akihisa Yamada, WST 2018 invited speakers

The Workshop on Termination (WST) traditionally brings together, in an
informal setting, researchers interested in all aspects of termination,
whether this interest be practical or theoretical, primary or derived.
The workshop also provides a ground for cross-fertilization of ideas from
the different communities interested in termination (e.g., working on
computational mechanisms, programming languages, software engineering,
constraint solving, etc.). The friendly atmosphere enables fruitful
exchanges leading to joint research and subsequent publications.

The workshop is held as part of the 2018 Federated Logic Conference
(FLoC 2018)

  http://www.floc2018.org/

IMPORTANT DATES:
 * submission deadline:  April 30, 2018
 * notification: May 28, 2018
 * final version due:    June 11, 2018
 * workshop: July 18-19, 2018

TOPICS: The 16th International Workshop on Termination welcomes
contributions on all aspects of termination. In particular, papers
investigating applications of termination (for example in complexity
analysis, program analysis and transformation, theorem proving, program
correctness, modeling computational systems, etc.) are very welcome.

Topics of interest include (but are not limited to):
 * abstraction methods in termination analysis
 * certification of termination and complexity proofs
 * challenging termination problems
 * comparison and classification of termination methods
 * complexity analysis in any domain
 * implementation of termination methods
 * non-termination analysis and loop detection
 * normalization and infinitary normalization
 * operational termination of logic-based systems
 * ordinal notation and subrecursive hierarchies
 * SAT, SMT, and constraint solving for (non-)termination analysis
 * scalability and modularity of termination methods
 * termination analysis in any domain (lambda calculus, declarative
   programming, rewriting, transition systems, etc.)
 * well-founded relations and well-quasi-orders

INVITED SPEAKERS:

    James Worrell - University of Oxford
   "Termination Checking and Invariant Synthesis for Affine Programs"

    Akihisa Yamada - NII Japan
   "Towards a Unified Method for Termination"


COMPETITION: Since 2003, the catalytic effect of WST to stimulate
new research on termination has been enhanced by the celebration
of the Termination Competition and its continuously developing
problem databases containing thousands of programs as challenges
for termination analysis in different categories, see

   http://termination-portal.org/wiki/Termination_Competition

In 2018, the Termination Competition will run in parallel with FLoC 2018.
More details will be provided in a dedicated announcement on the
competition.

PROGRAM COMMITTEE:
    Cristina Borralleras - U. de Vic
    Ugo Dal Lago - U. degli Studi di Bologna
    Carsten Fuhs - Birkbeck, U. of London
    Samir Genaim - U. Complutense de Madrid
    Juergen Giesl - RWTH Aachen
    Raul Gutiérrez - U. Politecnica de València
    Keiichirou Kusakari - Gifu University
    Salvador Lucas (chair) - U. Politecnica de Valencia
    Fred Mesnard - U. de La Reunion
    Aart Middeldorp - U. of Innsbruck
    Albert Rubio - U. Politecnica de Catalunya
    Rene Thiemann - U. of Innsbruck
    Caterina Urban - ETH Zürich

SUBMISSION: Submissions are short papers/extended abstracts which
should not exceed 5 pages. There will be no formal reviewing. In
particular, we welcome short versions of recently published articles
and papers submitted elsewhere. The program committee checks relevance
and provides additional feedback for each submission. The accepted
papers will be made available electronically before the workshop.

Papers should be submitted electronically via the submission page:

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

Please, use LaTeX and the LIPIcs style file

    http://drops.dagstuhl.de/styles/lipics/lipics-authors.tgz

to prepare your submission.

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] PPDP 2018: Deadline Extension!

[David Sabel]

News: The submission deadline is extended until Monday, May 8, 23:59 AoE!


==
    PPDP 2018: Deadline Extension
==
 20th International Symposium on
    Principles and Practice of Declarative Programming

 Frankfurt am Main, Germany, 3-5 September 2018

    http://ppdp-lopstr-18.cs.uni-frankfurt.de/ppdp18.html

    (co-located with LOPSTR 2018 and WFLP 2018)
 http://ppdp-lopstr-18.cs.uni-frankfurt.de
==



Invited Talks
=

-   Philippa Gardner, Imperial College: Testing and Verification for
    JavaScript (joint with LOPSTR)
-   Jorge Navas, SRI International: Constrained Horn Clauses for
    Verification (joint with LOPSTR)
-   Chung-Chieh Shan, University of Indiana: Calculating Distributions

Scope
=

The PPDP 2018 symposium brings together researchers from the declarative
programming communities, including those working in the functional,
logic, answer-set, and constraint handling 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 related to declarative
programming, 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; memory management.

-   Foundations: types; logical frameworks; monads and 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.

The PC chair will be happy to advise on the appropriateness of a topic.

PPDP will be co-located with the 28th Int'l Symp. on Logic-Based Program
Synthesis and Transformation (LOPSTR 2018).

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, but excluding bibliography). Work
that already appeared in unpublished or informally published workshop
proceedings may be submitted (please contact the PC chair in case of
questions). 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 5 pages **including references**.
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 general novel use of declarative programming in the classroom
programming pearl 

[Hol-info] 2nd CfP: Formal Techniques for Java-like Programs (FTfJP 2018) @ ECOOP/ISSTA 2018 in Amsterdam

[Summers Alexander John]

(Please distribute to interested PL parties - apologies for any cross postings)
Workshop website: 
https://conf.researchr.org/track/ecoop-issta-2018/FTfJP-2018-papers
Formal techniques can help analyze programs, precisely describe program 
behavior, and verify program properties. Languages such as Java, C#, and Scala 
are interesting targets for formal techniques due to their ubiquity and wide 
user base, stable and well-defined interfaces and platforms, and powerful (but 
also complex) libraries. New languages and applications in this space are 
continually arising, resulting in new PL research challenges.
Work on formal techniques and tools and on the formal underpinnings of 
programming languages themselves naturally complement each other. FTfJP is an 
established workshop which has run annually since 1999 alongside ECOOP, with 
the goal of bringing together people working in both fields. The workshop has a 
broad PL theme; the most important criterion is that submissions will generate 
interesting discussions within this community. Example topics of interest 
include:

  *   Language design and semantics
  *   Type systems
  *   Concurrency and new application domains
  *   Specification and verification of program properties
  *   Program analysis (static or dynamic)
  *   Security
  *   Pearls (programs or proofs)
FTfJP welcomes submissions on technical contributions, case studies, experience 
reports, challenge proposals, and position papers. Just as the number and the 
feature set of Java-like languages is expanding, the term "Java-like" should be 
interpreted broadly.

Submissions


Contributions related to formal techniques for Java-like programs are sought in 
two categories:

Full Papers. In 6 two-column pages, the paper should present a technical 
contribution, case study, or detailed experience report. We welcome both 
complete and incomplete technical results; ongoing work is particularly 
welcome, provided it is substantial enough to stimulate interesting discussions.

Short Papers. In 2 two-column pages, the paper should advocate a promising 
research direction, or otherwise present a position likely to stimulate 
discussion at the workshop. We encourage e.g. established researchers to set 
out a personal vision, and beginning researchers to present a planned path to a 
PhD.

Both types of contributions will benefit from feedback received at the 
workshop. Submissions will be peer reviewed, and will be evaluated based on 
their clarity and based on their potential to generate interesting discussions. 
The format of the workshop encourages interaction. FTfJP is a forum in which a 
wide range of people share their expertise, from experienced researchers to 
beginning PhD students.

Accepted papers will be published in the ACM Digital Library by default, though 
authors will be able to opt out of this publication, if desired. The use of 
ACM's template for the SIGPLAN 
format is required. At 
least one author of an accepted paper must attend the workshop to present the 
work and participate in the discussions.

Important Dates:

  *   Wed 9th May AOE: submission 
deadline
  *   Thu 14th Jun: acceptance notifications
  *   Sun 17th Jun: early registration deadline (for both main conferences and 
workshops)

Paper submission website: https://easychair.org/conferences/?conf=ftfjp2018

Program Committee

William J. Bowman (Northeastern University)
John Tang Boyland (University of Wisconsin-Milwaukee)
Mariangiola Dezani-Ciancaglini (Università di Torino, Italy)
Erik Ernst (Google, Aarhus)
Juliana Franco (Imperial College London)
Timothy Jones (Montoux)
Laura Kovacs (Vienna University of Technology, Austria and Chalmers University 
of Technology, Sweden)
Siddharth Krishna (New York University)
Oded Padon (Tel Aviv University)
Matthew Parkinson (Microsoft Research Cambridge)
Guido Salvaneschi (Technical University of Darmstadt)
Alexander J. Summers (ETH Zurich)
Elena Zucca (DIBRIS, University of Genova)

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info