[TYPES/announce] Verifying smart contracts for Blockchain

[Philip Wadler]

Verifying smart contracts for Blockchain
Supervisor: Professor Philip Wadler

The following PhD project is open for recruitment.
UK/EU/International applicants welcome.
https://web.inf.ed.ac.uk/cdt/cyber-security-privacy-and-trust-dtc/projects-open-for-recruitment

This work will develop techniques for specifying and verifying smart
contracts written in Plutus, the smart contract language of the
Cardano Blockchain. Ada, the cryptocurrency of Cardano, is a leading
cryptocurrency, in the top ten by market capitalisation.

Blockchain based technologies are a large and growing area
underpinning the rapid growth in digital finance and distributed
ledger technologies and markets. However, fundamental obstacles with
transaction time, trust and cost remain which restricts their
widespread adoption. One of the key problem areas to be addressed is
the verification of smart contracts. This PhD will develop techniques
for specifying and verifying smart contracts written in Plutus and
incorporated into a proof of concept prototype. This development of
this technology may have wider impact on other Blockchain variants
that support smart contracts, of which there are dozens.

The work will build on top of existing tools for specification and
verification, such as Agda or Coq. It is recognised by the industry
that there is little existing work on verification of smart
contracts. One of the most crucial questions is to understand what are
the most important properties to verify. Proposed properties include
preservation, ensuring that no currency is lost, and progress,
ensuring that the contract can always take a step (this last has also
been called liquidity). This research will seek to answer these
questions.

Please write to me <wadler at inf.ed.ac.uk>, explaining your interest and
your background in functional programming and formal methods.


== About the University of Edinburgh and LFCS ==

The University of Edinburgh School of Informatics brings together
world-class research groups in theoretical computer science,
artificial intelligence and cognitive science. The Informatics Forum,
opened in 2008, is located in central Edinburgh, Scotland's capital
and one of the best places to live in the UK. In the 2014 REF, the
School ranked as having produced more world-leading and
internationally excellent research (4* and 3*) than any other UK
university.

We welcome applications from members of groups traditionally
underrepresented in the field.  In 2013 and 2016, the School of
Informatics received an Athena Swan Silver Award, in recognition of
its commitment to advancing the careers of women in science,
technology, engineering, maths and medicine (STEMM) employment in
higher education and research.

The Laboratory for Foundations of Computer Science was established by
Burstall, Milner, and Plotkin in 1986, and is recognized worldwide for
groundbreaking research on topics in programming languages,
cryptography, semantics, type theory, proof theory, algorithms and
complexity, databases, security, and systems biology. We participate
in a thriving PL research community across Scotland, with Scottish
Programming Languages Seminars hosted every 3-4 months by PL groups at
Glasgow, Strathclyde, Heriot-Watt, St. Andrews, Dundee and Edinburgh.

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20201208/994e8554/attachment.htm>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20201208/994e8554/attachment.ksh>