[Haskell] Proof Engineers Wanted

[Gerwin Klein]

Data61 Seeking Proof Engineers
==
(applications close 15 October 2015)
http://ssrg.nicta.com.au/jobs/proof-engineers2015

If only there was a place where I could prove theorems for money, change the
world, and have fun while doing it...

Sounds too good to exist?

In the Trustworthy Systems team at Data61, formerly known as NICTA, that's
what we do for a living. We are the creators of seL4, the world's first fully
formally verified operating system kernel with extreme performance and strong
security & correctness proofs. Our highly international team is located on
the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia,
one of the world's most liveable cities.

We are looking for multiple motivated entry-level proof engineers who want to
join our team, move things forward, and have global impact. We are expanding
our team, because seL4 is going places. There are active projects around the
world in

 - Automotive - because cars have been hacked enough
 - Aviation - for more security and safety for autonomous vehicles
 - Connected consumer devices - with security built in from the start
 - SCADA - for more secure intelligent industrial control automation
 - Spaceflight, autonomous and crewed - because awesome

To make these projects successful, we need to scale formal verification.
You would

 - work on industrial-scale formal proofs in Isabelle/HOL
 - help to extend and improve existing proofs or verify new features in seL4
 - contribute to improved proof automation and better reasoning techniques
 - apply formal proof to real-world systems and tools

To apply for this position, you should possess a significant subset of the
following skills.

 - functional programming in a language like Haskell, ML, or OCaml
 - first-order or higher-order formal logic
 - basic experience in C
 - ability and desire to quickly learn new techniques
 - undergraduate degree in Computer Science, Mathematics, or similar
 - ability and desire to work in a larger team

If you additionally have experience

 - in software verification with an interactive theorem prover such as
   Isabelle/HOL or Coq, and/or
 - with operating systems and microkernels

you should definitely apply!

If you have the right skills and background, we can provide training on the job.
Continual learning is a central component of everything we do. You will work
with a unique world-leading combination of OS and formal methods experts,
students at undergraduate and PhD level, engineers, and researchers from 5
continents, speaking over 15 languages. Trustworthy Systems is a fun,
creative, and welcoming workplace with full health insurance and flexible
hours & work arrangements.

We value diversity in all forms and welcome applications from people
of all ages, including people with a disability, and those who identify as
LGBTIQ. See http://ssrg.nicta.com.au/diversity/ for more information.

The salary range for this position is AUD 65,000 to 90,000 for recent
graduates, depending on experience and qualification.

Apply by sending your CV, undergraduate transcript (if applicable), two
references, and cover letter to  and
.


This round of applications closes 15 October 2015.

The seL4 code and proof are open source. Check them out at
https://github.com/seL4

More information about NICTA's Trustworthy Systems team at
http://ssrg.nicta.com.au


Still studying? We also have internship opportunities!
http://ssrg.nicta.com.au/students/





The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
Haskell mailing list
Haskell@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell

[Haskell] Call for Papers: ITP 2014

[Gerwin Klein]

 Call for Papers

ITP 2014
  5th International Conference on Interactive Theorem Proving 
 14th-17th July 2014 in Vienna, Austria 
  http://www.cs.uwyo.edu/~ruben/itp-2014

IMPORTANT DATES

Abstract submission:   24th January 2014
Paper submission:  31st January 2014
Author notification:   21st March 2014
Camera-ready:  18th April 2014
Conference:14th-17th July 2014


CONFERENCE BACKGROUND

ITP is the premier international conference for researchers from all areas of
interactive theorem proving and its applications. It represents the natural
evolution of the TPHOLs conference series to include research related to all
other interactive theorem provers. TPHOLs meetings took place every year from
1988 until 2009. In 2010, the first ITP conference was held in Edinburgh,
Scotland, as part of the Federated Logic Conference (FLoC). Subsequent ITP
conferences were held in Nijmegen, The Netherlands, in 2011, Princeton, New
Jersey, USA, in 2012, and Rennes, France in 2013. ITP 2014 will again be a
part of FLoC, in Vienna, Austria.


PAPER SUBMISSIONS

ITP welcomes submissions describing original research on all aspects of
interactive theorem proving and its applications. In particular, the ITP
community is open to users of all interactive theorem provers. Suggested
topics include but are not limited to the following:

 - formal aspects of hardware and software,
 - formalizations of mathematics,
 - improvements in theorem prover technology,
 - user interfaces for interactive theorem provers,
 - formalizations of computational models,
 - use of theorem provers in education,
 - industrial applications of interactive theorem provers, and
 - concise and elegant worked examples of formalizations (Proof Pearls).

Submissions must be made electronically in PDF format. Submissions should be
prepared using the Springer LNCS format, available from
http://www.springer.com/computer/lncs/lncs+authors, and submitted via
EasyChair. Submissions must describe original unpublished work not submitted
for publication elsewhere, presented in a way that is accessible to users of
other systems. The proceedings will be published as a volume in the Springer
Lecture Notes in Computer Science series and will be available to participants
at the conference.

ITP accepts both long papers (up to 16 pages) and rough diamonds (up to six
pages, possibly in the form of an extended abstract). Both categories of
papers will be fully refereed and included in the published proceedings.
Papers in the rough diamonds category are expected to present innovative and
promising ideas that have not yet had the time to mature. Regular papers are
expected to present mature research projects with appropriate supporting
evidence.

All papers should have an abstract of approximately 100 words. Note that
abstracts must be submitted a week prior to the paper submission deadline.
Papers should also include a list of relevant keywords, which must include the
name of the theorem prover featured in the paper. We strongly encourage
submissions that describe interactions with or improvements of a theorem
prover. Authors of such papers should provide verifiable evidence of an
implementation, such as appropriate source files. This material may be
uploaded via EasyChair or may be placed online, as long as a URL is included
with the submission.

Authors of accepted papers are expected to present their papers at the
conference, and will be required to sign copyright release forms. All
submissions must be written in English.


ORGANIZATION

Program Chairs
Gerwin Klein, NICTA and The University of New South Wales, Australia
Ruben Gamboa, University of Wyoming, USA

Workshop Chair
David Pichardie, INRIA, France

Program Committee
Jeremy Avigad, Carnegie Mellon University
Lennart Beringer, Princeton University
Yves Bertot, INRIA
Thierry Coquand, Chalmers University
Amy Felty, University of Ottawa
Ruben Gamboa, University of Wyoming
Georges Gonthier, Microsoft Research
Elsa Gunter, University of Illinois at Urbana-Champaign
John Harrison, Intel Corporation
Matt Kaufmann, University of Texas at Austin
Gerwin Klein, NICTA and UNSW
Alexander Krauss, Technische Universität München
Ramana Kumar, University of Cambridge
Joe Leslie-Hurd, Intel Corporation
Assia Mahboubi, INRIA - École polytechnique
Panagiotis Manolios, Northeastern University
Magnus O. Myreen, University of Cambridge
Tobias Nipkow, TU München
Michael Norrish, NICTA
Sam Owre, SRI International
Christine Paulin-Mohring, Université Paris-Sud
Lawrence Paulson, University of Cambridge
David Pichardie, INRIA Rennes - Bretagne Atlantique
Lee Pike, Galois, Inc.
Jose-Luis Ruiz-Reina, University of Seville
Julien Schmaltz, Open University of the Netherlands
Bas Spitters, Radboud University Nijmegen
Sofiene Tahar, Concordia University
René Thiemann, University of Innsbruck
Laurent Théry, INRIA
Christian Urban, King's College

Re: [Haskell] Specification and prover for Haskell

[Gerwin Klein]

On 25/10/2010, at 7:09 PM, Romain Demeyer wrote:
 I'm working on static verification in Haskell, and I search for existing 
 works on specification of Haskell programs (such as pre/post conditions, for 
 example) or any other functional language.

We have used Haskell extensively in the verification of the seL4 microkernel. 
One part of that was translating a prototype of the kernel into Isabelle and 
proving a large number of invariants as well as proving two refinement theorems 
about the translation. For our work the translation itself was not correctness 
critical, so we were happy to use our own somewhat ad-hoc tool for it.

Some papers on this are:

Pre/post verification and refinement of state monad programs:
http://www.cse.unsw.edu.au/~kleing/papers/Cock_KS_08.html

Experience report on the Haskell verification:
http://www.cse.unsw.edu.au/~kleing/papers/Klein_DE_09.html

The whole picture:
http://www.cse.unsw.edu.au/~kleing/papers/sosp09.html

More papers here: 
http://www.ertos.nicta.com.au/research/l4.verified/pubs.pml

In general, if your program does not use state monads, but is just a simple, 
straightforward functional program, the combination of Haskabelle and 
Isabelle/HOL can work quite nicely without a big formal apparatus such as a 
pre/post calculus. You can just state properties directly as you might in 
quickcheck.


 It would be great if there exists a prover based on this kind of 
 specifications. I already found the ESC/Haskell. Do you know some other works 
 which could be interesting?

We're using Isabelle/HOL. In the work above this was together with our own 
translator from Haskell to Isabelle, in the future it will possibly Haskabelle 
which has already been pointed out.

Cheers,
Gerwin

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] translating Haskell into theorem provers

[Gerwin Klein]

Thanks for all the replies I got, they have been helpful!

Cheers,
Gerwin
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] translating Haskell into theorem provers

[Gerwin Klein]

Hi,

is any of you aware of activities that aim to translate Haskell into 
interactive theorem provers like PVS or Isabelle/HOL? (automatically or 
manually).

We know about the Programatica project and Brian Huffman's work, but turned 
up little else.

Cheers,
Gerwin

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell