coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Interactive theorem proving: 3 Postdoctoral positions at Cambridge

From: Lawrence Paulson <lp15 AT cam.ac.uk>
To: isabelle-users <isabelle-users AT cl.cam.ac.uk>, hol-info AT lists.sourceforge.net, coq-club AT inria.fr
Subject: [Coq-Club] Interactive theorem proving: 3 Postdoctoral positions at Cambridge
Date: Fri, 26 May 2017 16:32:41 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lp15 AT cam.ac.uk; spf=Pass smtp.mailfrom=lp15 AT cam.ac.uk; spf=Pass smtp.helo=postmaster AT ppsw-30.csi.cam.ac.uk
Ironport-phdr: 9a23:60WSyRXo89gRiN/AAP/1HvQVFMzV8LGtZVwlr6E/grcLSJyIuqrYbBKAt8tkgFKBZ4jH8fUM07OQ6PG+HzFfqdbZ6TZZIcMKD0dEwewt3CUeQ+e9SnfHZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/2O+94YDcbBtVjzShf7xyMA+2rQLMvcUKnIduMKg8xx/Ir3dSe+lbx35jKVaPkxrh/Mu98ppu/iZKt/4968JMVLjxcrglQ7BfEDkpPGc56dHxuxXEUQWB+GYXXH8MkhpPDQjF7RX6UYn0vyDnqOdz2zSUMNPvQ7wsVjus86lkSBnziCcaLDE5633YitZxjK1Avh2soQF0zpPOb4GUMPp+eb7dfc8fSGFcUMtdSzBND4WhZIYJEuEPP/tXr5PlqlUOsRSwCgajCv7sxDFGmHH42rY30/g4EQHDwAAgH84CvGrSod7oNKkSS+e1zKzQwDvFdfxX1y3955bOch89v/6HQKh+ftDMyUkrDAPFiVOQopHiMjORzuQBrmiW4vF8Wu21jm4rsRt+rSS1yscxiYnEn4QYwU3K+yV+xYY6P9y4SEhjbNG4CpRQsjuWOJFqTc84XmFouyA3waAFt56jZCUG1ZoqywPFZ/CaboSE/wjvWeWLLTtlin9pZKqziwus/UWj0OHwSMe53EhQoidFk9TArH8A2wLV58OaUPVy5F2h1iyK1w3L6uFLP0Q0la3DJp452r4wjZQSvV3NEyPqgkn5kLSWdkQ+9ue08evnZ6/qqYWAOINulwH+Mbwims25AesmLggDR3WX9Oqh2LH54EH1XahGguc1n6XDrZzXK9gXqra8AwBP04Yj7xi/Dy2h0NQdhXQHKEpFdA+HgoXyJ17BOvX4Ae2ljFuwijtr2vPGMqX7AprRNnjDjKvhfbFl5kFAzwoz1MlT6I5QCrEcO/3+QVTxtdzdDh8hKQO42efnCNNn1oMfQ22DGKGZMLmB+WOPs+M0KuOBYIsY/SvmJuI+r6rvlnYzlFsZcOy0xpYNc1izGrJtKkDfaHGqn9RXVS8KuQ57Terkj3WGUCVPfDCpWL8m7Tw1D5ipAMHFS5zpyLeGxWKwGoBcTmFAEFGFV3nyJKueXPJZTCuNOMJnmTFMbbG8T5Qm01n6sBejlpJsJ++S8yZeqJG1h4s93PHaiRxnrW88NM+ayWzYF2w=

ALEXANDRIA is a five-year ERC-funded project aimed at making interactive
theorem proving useful in mathematical research. The workplan includes pilot
studies to identify critical issues, library development and the
implementation of advanced search, perhaps using machine learning. Two
mathematicians and an Isabelle architect will be hired. Official descriptions
of the vacancies are online:

http://www.jobs.cam.ac.uk/job/13866/
http://www.jobs.cam.ac.uk/job/13867/

We can look forward to some exciting developments! And while this project
will be based on Isabelle, I also hope for fruitful cooperation with users of
other systems.

Larry Paulson

Computer Laboratory, University of Cambridge
Cambridge CB3 0FD, England
Tel: +44(0)1223 334623

[Coq-Club] Interactive theorem proving: 3 Postdoctoral positions at Cambridge, Lawrence Paulson, 05/26/2017