Logic List Mailing Archive

Various PhD student funding opportunities in theoretical computer Science, Swansea (Wales), Deadline: 22 Jan 2018

The CS department of Swansea University is inviting applications for a 
fully funded PhD studentship, for start in October 2018 or January 2019. 
We would be grateful if you could forward this message to potential 
candidates. Applicants should hold an MSc or equivalent in a relevant 
subject at the starting time, and be UK/EU citizens. The application 
deadline is January 22nd, 2018. Ideally, applicants will get in touch with 
the prospective supervisor well in advance.

There are a number of available projects (see http://www.swansea.ac.uk/ 
science/research/dtc/computer-science-projects-2018-19/ for the full 
list). The logic related ones are copied in below. The prospective 
supervisors will gladly give more information to potential applicants.

In order to be eligible for funding, applications should be submitted 
under the umbrella project

http://www.swansea.ac.uk/postgraduate/scholarships/ 
research/science-sures-phd-comp-sci-putting-theory-into-practice.php



*CS 1 - Project Title: Verification of Bitcoins and other Cryptocurrencies.*

    - First Supervisor Name:  Anton Setzer
    - Email Address: a.g.setzer@swansea.ac.uk
    - Link to Staff Profile: http://www.swansea.ac.uk/staff/science/computer-
    science/a.g.setzer/

*Project Description: *

This project would connect well with research by Pedro Helles in the School
of Law on smart contracts and cryptocurrencies. While there has been a lot
of interest in the media in Bitcoins, with the price for Bitcoins
increasing from 1003 US-$ on 1/1/2017 to 8155 US-$ at time of writing,
there exist no formal proof yet  that the protocol is actually correct,
which is worrying, since Bitcoins rely entirely on the algorithm with no
human organisation mediating it. The goal of this project is  to fix this
gap, and to formally verify the Bitcoin protocol and protocols of other
cryptocurrencies in the interactive theorem proving tool Agda.



*CS 2 - Project Title: Development of a language for writing smart
contracts.*

    - First Supervisor Name:  Anton Setzer
    - Email Address: a.g.setzer@swansea.ac.uk
    - Link to Staff Profile: http://www.swansea.ac.uk/staff/science/computer-
    science/a.g.setzer/

*Project Description: *

This project would connect well with research by Pedro Helles in the School
of Law on smart contracts and cryptocurrencies. Smart contracts allow to
formalise contractual relationships regarding exchange of money using
cryptocurrencies in a purely algorithmic way without any involvement of
legal entities, but can lead to loss of money as in the DAO attack on
Ethereum, where the loss of 100 Million US-$ was only avoided by creating a
hard fork, violating the principle that cryptocurrencies are entirely
governed by algorithms. The goal of this project is to develop based on the
interactive theorem prover Agda a language for smart contracts, in which
correctness proofs can be carried out, and therefore contractors can rely
on the correctness of their contracts.


*CS 3 - Project Title: Beyond sigma-frames*

    - First Supervisor Name: Arno Pauly (Director of Study Anton Setzer)
    - Email Address: a.m.pauly@swansea.ac.uk
    <https://mobile.swan.ac.uk/owa/redir.aspx?C=SNHn-ApK2iag4NMDddwtfJJoR9q-CPfzEQtwfZ49W8FWr6GmPjPVCA..&URL=mailto%253aa.m.pauly%2540swansea.ac.uk>
    - Link to Staff Profile: http://www.swansea.ac.uk/staff/science/computer-
    science/paulya/
    <https://mobile.swan.ac.uk/owa/redir.aspx?C=c5PzeYUjRjz8IDuZeYPiFrp6RHtZ7Z8Sqhu7gzjehe5Wr6GmPjPVCA..&URL=http%253a%252f%252fwww.swansea.ac.uk%252fstaff%252fscience%252fcomputer-science%252fpaulya%252f>

*Project Description: *

In formal topology, the notion of a frame is studied as an abstraction of
the collection of open subsets of a topological space. While the opens of a
frame are closed under arbitrary unions and finite intersections, this is
relaxed to closure under countable unions and finite intersection to obtain
the notion of a sigma-frame. In this project, variations of frames with
specific closure properties will be studied in order to make formal
topology applicable to descriptive set theory.


*CS 4 - Project Title: Computational complexity and bounded rationality*

    - First Supervisor Name: Arno Pauly (Director of Study Arnold Beckmann)
    - Email Address: a.m.pauly@swansea.ac.uk
    <https://mobile.swan.ac.uk/owa/redir.aspx?c=ervaoeoeprivyrdapoomba9fbbvtulh9gtjw_eliv6xgdeuqqtpvca..&url=mailto%253aa.m.pauly%2540swansea.ac.uk>
    - Link to Staff Profile: http://www.swansea.ac.uk/staff/science/computer-
    science/paulya/
    <https://mobile.swan.ac.uk/owa/redir.aspx?C=M_lNdYGYOKo891yxM8Wk50esAC7pu_hvaiiUT_EPHyrGDeuqQTPVCA..&URL=http%253a%252f%252fwww.swansea.ac.uk%252fstaff%252fscience%252fcomputer-science%252fpaulya%252f>

*Project Description: *

If figuring out the best way to play a game is too complicated to be
feasible, what is the next best approach? This project combines
computational complexity and algorithmic game theory to search for a notion
of rational behaviour under complexity constraints. This is a step towards
bridging the gap between mathematical theory and experimental observations
in game theory.



* CS 9 - Project Title: Algorithms for very hard satisfiability problems
(SAT)*

    - First Supervisor Name: Oliver Kullmann
    - Email Address: O.Kullmann@Swansea.ac.uk
    - Link to Staff Profile: http://www.swansea.ac.uk/staff/science/computer-
    science/o.kullmann/
    <https://mobile.swan.ac.uk/owa/redir.aspx?C=Cv0uO0EwHnKNIxPA9OMceXujPiT_aJ2BfFW3GH9PVIAIYLbgPzPVCA..&URL=http%253a%252f%252fwww.swansea.ac.uk%252fstaff%252fscience%252fcomputer-science%252fo.kullmann%252f>

*Project Description:*

The article "The Science of Brute Force",
Communications of the ACM, Vol. 60 No. 8, gives an overview on exciting new
developments in the area of solving hard computational problems, via
SAT solving. The PhD can be about the theory, implementations,
applications, or any combination thereof, of algorithms and the underlying
problem structures, focussing on hard SAT problems.



*CS 10 - Project Title: Combinatorics of Satisfiability*

    - First Supervisor Name: Oliver Kullmann
    - Email Address: O.Kullmann@Swansea.ac.uk
    - Link to Staff Profile: http://www.swansea.ac.uk/staff/science/computer-
    science/o.kullmann/
    <https://mobile.swan.ac.uk/owa/redir.aspx?C=Cv0uO0EwHnKNIxPA9OMceXujPiT_aJ2BfFW3GH9PVIAIYLbgPzPVCA..&URL=http%253a%252f%252fwww.swansea.ac.uk%252fstaff%252fscience%252fcomputer-science%252fo.kullmann%252f>

*Project Description:*

Solving boolean systems of equations (the SAT problem) and combinatorics
have deep connections, and a theory of SAT is emerging. This PhD will be
about strengthening these connections, developing new synergies with
mathematics, combinatorics, complexity theory and algorithmics.


*CS 15 - Project Title: Computing with Infinite Data *

    - Supervisor: Ulrich Berger
    - Email: u.berger@swansea.ac.uk
    - Link to Staff Profile: http://cs.swansea.ac.uk/~csulrich/

*Project Description:*

Infinite or virtually infinite data occur naturally when processing very
large data sets or exact real numbers, and computing with such data poses
many theoretical and practical challenges.  Computing with Infinite Data
(CID,http://cordis.europa.eu/project/rcn/207017_en.html,
http://www.cs.swansea.ac.uk/theory/index.php/cid/
<https://mobile.swan.ac.uk/owa/redir.aspx?C=BdzQIgWf_0pDbNoPrAMsK1SXm-vagKBcfNurrRXjMhkqLiWxUjPVCA..&URL=http%253a%252f%252fwww.cs.swansea.ac.uk%252ftheory%252findex.php%252fcid%252f>)
is a four year Horizon 2020 project, starting in April 2017, that will
provide the opportunity and means for two PhD students to spend several
months abroad in order to facilitate research and knowledge exchange in
that area.  The proposed research will focus on logical methods for the
specification and extraction of formally verified algorithms for infinite
data.
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/

provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam