[TYPES/announce] Ph.D. position in Mathematical Foundations of Computation in Bath
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Mathematical Foundations group at the University of Bath is offering a Ph.D. position in foundations of computation: Computational and representational aspects of modern proof systems In developing the mathematical foundations of computation, a central insight is that formal proofs can be viewed as computer programs. In this direction, a recent discovery by members of the group, in collaboration with international colleagues, is a correspondence between modern proof methods and computation over geometric objects. The position will be part of a larger project to further develop this connection. The particular task will be to develop and investigate computational calculi arising from this correspondence. The Mathematical Foundations group is a diverse and active research community within the Department of Computer Science. The group is world-class in the area of logic and semantics, and is internationally well-connected. Its members have an excellent record of supervising Ph.D. candidates, many of whom have gone on to establish themselves as successful independent researchers. The prospective supervisor for the advertised position is Willem Heijltjes. Relevant links: Willem Heijltjes - http://www.cs.bath.ac.uk/~wbh22/ Mathematical Foundations - http://www.bath.ac.uk/comp-sci/research/mathematical-foundations/ Details: Starting date for the position is 1st of October 2013. The position is funded by a three-year Graduate School studentship. It comprises full Home/EU tuition fees and a training support grant, plus a stipend of £13,590 per annum (2012/13 rate). How to apply: Closing date for the advertisement is 28th of February 2013. Candidates must have a bachelor's degree or higher in mathematics, computer science, or a related field, or be expected to graduate before the starting date. Non-native English speakers will be required to obtain a satisfactory TOEFL or IELTS test score before the starting date. The application process further requires the contact details of two academic referees. To apply, please go to the page below and follow the steps outlined there. http://www.bath.ac.uk/science/gradschool/applying/ On the page Choosing your programme of study, please make sure to select PhD Programme in Computer Science (full-time) under Department of Computer Science. Enquiries: Please contact Willem Heijltjes w.b.heijlt...@bath.ac.uk
[TYPES/announce] Structures and Deduction 2014 - call for participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PARTICIPATION The Third International Workshop on STRUCTURES AND DEDUCTION (SD14) 12 July 2014 Affiliated with CSL-LICS at FLOC 2014 Part of the Vienna Summer of Logic http://vsl2014.at/sd/ This is the third in a series of meetings that bring together researchers in different areas of proof theory. The main interest is in new algebraic and geometric results in proof theory that expand our abilities to manipulate proofs, that help to reduce bureaucracy in deductive systems, and that ultimately lead to new methods for proof search and new kinds of proof certificates. Invited speakers Gilles Dowek (Inria Paris-Rocquencourt) Rosalie Iemhoff (Utrecht University) Kazushige Terui (Kyoto University) Contributed talks http://www.easychair.org/smart-program/VSL2014/SD-accepted.html Programme http://www.easychair.org/smart-program/VSL2014/SD-program.html Registration http://vsl2014.at/registration/ (early registration deadline: 8 June) The workshop is found under: Week 1 of FLOC, Workshop Block 1, one day workshops - July 12. We look forward to seeing you in Vienna! Kaustuv Chaudhuri Willem Heijltjes Lutz Strassburger
[TYPES/announce] PhD position "Efficient and natural proofs and algorithms" at University of Bath
[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
We are recruiting for a PhD position "Efficient and natural proofs and
algorithms"
Funding: Competition funded (EU/UK)
Deadline: 31 October 2018 - early application recommended
Start:Before 1 April 2019
People: Dr. Alessio Guglielmi a.guglie...@bath.ac.uk
Dr. Willem Heijltjesw.b.heijlt...@bath.ac.uk
Mathematical Foundations Group
Department of Computer Science
University of Bath
= Description =
Proofs and algorithms are everyday objects in our discipline, but they are
still very mysterious. Suffice to say that we are currently unable to decide
whether two given proofs or two given algorithms are the same; this is an old
problem that dates back to Hilbert. Also, proofs and algorithms are intimately
connected in the most famous open problem in mathematics: P vs NP.
We make progress by trying to unveil the fundamental structure behind proofs
and algorithms, what we call their semantics. In other words, we are interested
in the following questions:
What is a proof?
What is an algorithm?
How can we define them so that they have efficient and natural semantics?
The questions above are interesting in their own right, but we note that
answering them will enable technological advances of great impact on the
society and the economy. For example, it will be possible to build a worldwide,
universal tool for developing, validating, communicating and teaching
mathematics. Also, quickly producing provably bug-free and secure software will
become possible, so solving one of the most complex and important open
engineering problems.
In order to understand proofs and algorithms we create new mathematics starting
from proof theory and semantics. The methods we use are mostly discrete,
algebraic and combinatorial, but there is a growing geometrical component. The
recent advances which our methods are mostly based on are linear logic, game
semantics and deep inference.
You can find more information at
http://alessio.guglielmi.name/res/cos/
Our group is very well financed via several grants. Thanks to our international
relations, working with us means having a truly multicultural experience
together with all the researchers at the forefront of this worldwide research
effort. As a result, all our graduates work and publish at the highest level.
The facilities at the University of Bath are outstanding and the city is so
beautiful that UNESCO recognises it as a World Heritage Site.
= Contact =
For questions about the project or the application process, please contact us:
Alessio Guglielmi a.guglie...@bath.ac.uk
Willem Heijltjesw.b.heijlt...@bath.ac.uk
= How to apply =
Applicants should hold, or expect to gain, a First Class or good Upper Second
Class Honours degree, or the equivalent from an overseas university. A master’s
level qualification would also be advantageous.
Formal applications should be made via the University of Bath’s online
application form for a PhD in Computer Science:
https://samis.bath.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app=RDUCM-FP01=0013
Application deadline: 31 October 2018.
Note: We are hoping to fill this position as quickly as possible and
applications may close earlier than the advertised deadline if a suitable
candidate is found; early application is therefore recommended.
Start date: negotiable, but by 1 April 2019 at the latest.
See also the advertisement here:
https://www.findaphd.com/search/ProjectDetails.aspx?PJID=100543
= Funding =
Research Council funding is available on a competition basis to Home and EU
students who have been resident in the UK for 3 years prior to the start of the
project. For more information on eligibility, see:
https://epsrc.ukri.org/skills/students/help/eligibility/
Funding will cover Home/EU tuition fees, a stipend (£14,777 per annum for
2018/19) and a training support fee of £1,000 per annum for 3.5 years.
Applicants classed as Overseas for tuition fee purposes are NOT eligible for
funding; however, we welcome all-year-round applications from self-funded
candidates and candidates who can source their own funding.
[TYPES/announce] Post-doctoral position "Typed lambda-calculi with sharing and unsharing" at University of Bath
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We invite applications for a post-doctoral research position, to investigate a new approach to sharing in the lambda-calculus based on deep-inference proof theory. This is a 3-year fixed-term post starting 1st of January 2019, part of the EPSRC-funded project `Typed Lambda-Calculi with Sharing and Unsharing'. Deadline: 29 October 2018 Start: 1 January 2019 Duration: 3 years Salary: Grade 7 - £33,199 rising to £39,609 Vacancy:http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=KM6179 Project:http://willem.heijltj.es/Unsharing Enquiries: w.b.heijlt...@bath.ac.uk Department of Computer Science University of Bath United Kingdom = Description = In recent years, deep inference has made a large impact in proof theory, with spectacular results in proof complexity and normalization for classical logic. In this project we investigate intuitionistic deep inference from a computational perspective, starting from the exciting observation that it can express forms of sharing thus far seen only in sharing graphs for optimal lambda-calculus reduction. We will build on this observation to: develop a theory of normalization with sharing in deep inference, possibly capturing optimality; implement the new means of sharing in typed lambda-calculi, graph-rewriting calculi, and abstract machines; measure their efficiency with semantic tools such as quantitative types. We are looking for excellent candidates with a PhD and a proven track record in one or more of the following areas: * Structural proof theory, particularly deep inference * Sharing in the lambda-calculus * Sharing graphs and optimal reduction * Denotational semantics, particularly quantitative semantics You will be part of the Mathematical Foundations group in the Department of Computer Science, University of Bath. We are a small, lively research group with an excellent international reputation. You will have the opportunity to travel to various collaborators on the project in Europe, for example in Bologna, Oslo, and Paris. The University of Bath is a great place to work with outstanding facilities. Bath is a Unesco World Heritage city with fantastic amenities offering excellent quality of life. = Relevant links = Project page http://willem.heijltj.es/Unsharing Mathematical Foundations group http://www.bath.ac.uk/comp-sci/research/mathematical-foundations/ Deep Inference http://alessio.guglielmi.name/res/cos/ = Applications = To apply, use the online form on the vacancy page. Vacancy http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=KM6179 Job Description & Person Specification (MS WORD) http://www.bath.ac.uk/jobs/Upload/vacancies/files/13812/Job%20description%20RA.docx (PDF) http://willem.heijltj.es/Unsharing/pdf/Job_description_Unsharing.pdf Applications close 29 October. Interview dates are to be determined. Please also consider the following. Terms of Employment http://www.bath.ac.uk/jobs/display.aspx?id=1201=0 = Enquiries = For any questions about the position, the project, or the recruitment process, please contact: Willem Heijltjes Department of Computer Science University of Bath w.b.heijlt...@bath.ac.uk http://willem.heijltj.es
[TYPES/announce] Lecturer (assistant professor) position in Bath
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The University of Bath is hiring a lecturer (assistant professor) in Computer Science. We are looking in particular for strong candidates to join our Mathematical Foundations group: http://www.bath.ac.uk/projects/mathematical-foundations-of-computation/ The vacancy and online application form are here: http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=CC7055 Note the deadline: 20 October 2019 The post is a replacement for John Power, who retired this summer. Though it is open to the other research areas in the department (HCI, Graphics & Vision, AI), we expect to prioritise excellent candidates who complement our current specialities in the Mathematical Foundations area: * Computer Algebra * Cryptography * Lambda-calculus * Proof Theory * Real Algebraic Geometry * Semantics For any questions about the post or the recruitment process, please contact: Alessio Guglielmi Willem Heijltjes
[TYPES/announce] PhD position "Efficient and natural proofs and algorithms" at University of Bath
[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
We are recruiting for a PhD position "Efficient and natural proofs and
algorithms"
Funding: Competition funded (EU/UK)
Deadline: 9 February 2020
Start:28 September 2020 (anticipated)
People: Dr. Alessio Guglielmi a.guglie...@bath.ac.uk
Dr. Willem Heijltjesw.b.heijlt...@bath.ac.uk
Mathematical Foundations Group
Department of Computer Science
University of Bath
= Description =
Proofs and algorithms are everyday objects in our discipline, but they are
still very mysterious. Suffice to say that we are currently unable to decide
whether two given proofs or two given algorithms are the same; this is an old
problem that dates back to Hilbert. Also, proofs and algorithms are intimately
connected in the most famous open problem in mathematics: P vs NP.
We make progress by trying to unveil the fundamental structure behind proofs
and algorithms, what we call their semantics. In other words, we are interested
in the following questions:
What is a proof?
What is an algorithm?
How can we define them so that they have efficient and natural semantics?
The questions above are interesting in their own right, but we note that
answering them will enable technological advances of great impact on the
society and the economy. For example, it will be possible to build a worldwide,
universal tool for developing, validating, communicating and teaching
mathematics. Also, quickly producing provably bug-free and secure software will
become possible, so solving one of the most complex and important open
engineering problems.
In order to understand proofs and algorithms we create new mathematics starting
from proof theory and semantics. The methods we use are mostly discrete,
algebraic and combinatorial, but there is a growing geometrical component. The
recent advances which our methods are mostly based on are linear logic, game
semantics and deep inference.
You can find more information at
http://alessio.guglielmi.name/res/cos/
http://www.bath.ac.uk/projects/mathematical-foundations-of-computation/
Our group is very well financed via several grants. Thanks to our international
relations, working with us means having a truly multicultural experience
together with all the researchers at the forefront of this worldwide research
effort. As a result, all our graduates work and publish at the highest level.
For example, one of our recent PhDs, Anupam Das, has won a prestigious UKRI
Future Leaders Fellowship in 2019, worth £1.5M. The facilities at the
University of Bath are outstanding and the city is so beautiful that UNESCO
recognises it as a World Heritage Site.
= Contact =
For questions about the project or the application process, please contact us:
Alessio Guglielmi a.guglie...@bath.ac.uk
Willem Heijltjesw.b.heijlt...@bath.ac.uk
= How to apply =
Applicants should hold, or expect to gain, a First Class or good Upper Second
Class Honours degree in Mathematics or Computer Science, or the equivalent from
an overseas university. A master’s level qualification would be advantageous.
Formal applications should be made via the University of Bath’s online
application form for a PhD in Computer Science:
https://samis.bath.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app=RDUCM-FP01=0014
Anticipated start date: 28 September 2020.
= Funding =
Research Council funding is available on a competition basis to Home and EU
students who have been resident in the UK for 3 years prior to the start of the
project. For more information on eligibility, see:
http://epsrc.ukri.org/skills/students/guidance-on-epsrc-studentships/eligibility/
Funding will cover Home/EU tuition fees, a stipend (£15,009 per annum for
2019/2020) and a training support grant of £1,000 per annum for 3.5 years.
Applicants classed as Overseas for tuition fee purposes are NOT eligible for
funding; however, we welcome all-year-round applications from self-funded
candidates and candidates who can source their own funding.
[TYPES/announce] PhD positions in Mathematical Foundations of Computation at University of Bath
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are recruiting for 2 PhD positions Funding: Competition funded Deadline: Sunday 21 February 2021 Start:October 2021 (anticipated) Mathematical Foundations Group Department of Computer Science University of Bath = The Mathematical Foundations group = Our group explores some of the deepest topics in logic and their relation to the theory of computation. We establish bridges between proof theory, category theory, semantics and complexity, so that the methods of each discipline enrich the others. We design new theories and solve old problems. For example, we defined a new proof formalism, called 'open deduction', that allowed us to describe one of the most efficient known notions of computation for the lambda-calculus. That was made possible by introducing ideas from complexity theory and category theory into proof theory and its computational interpretations. Our research programme, in a nutshell, is to help develop the mathematics of computation. This matters at least for two reasons. The first is that computing, at present, is art, not engineering. Indeed, because of the lack of mathematics, software correctness is not guaranteed the same way a bridge is guaranteed to stand, for example. The second reason is that the theory of computation is rapidly becoming one of the most important intellectual achievements of civilisation. For example, it is now helping physics and biology create new models in their domain. Because of all that, our doctoral graduates have embarked on excellent academic careers in some of the most intellectually rewarding and innovative branches of research, and will continue to do so. Our webpage: https://www.bath.ac.uk/projects/mathematical-foundations-of-computation/ Please see at the end of this email for a list of projects and supervisors. = Contact = For questions about the project or the application process, please contact us, Alessio Guglielmi a.guglie...@bath.ac.uk Willem Heijltjesw.b.heijlt...@bath.ac.uk or one of the supervisors of the projects at the end of this email. = How to apply = Applicants should hold, or expect to gain, a First Class or good Upper Second Class Honours degree in Mathematics or Computer Science, or the equivalent from an overseas university. A master’s level qualification would be advantageous. Formal applications should be made via the University of Bath’s online application form for a PhD in Computer Science: http://samis.bath.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app=RDUCM-FP01=0015 You would apply to a specific project and supervisor from the list at the end of this email. More information on the general applications process is here: http://www.bath.ac.uk/guides/how-to-apply-for-doctoral-study/ Non-UK applicants will also be required to have met the English language entry requirements of the University of Bath: http://www.bath.ac.uk/corporate-information/postgraduate-english-language-requirements-for-international-students/ Anticipated start date: Monday 4 October 2021 = Funding = Candidates applying for this project may be considered for a 3.5-year studentship from the Engineering and Physical Sciences Council (EPSRC DTP). Funding covers tuition fees, a stipend (£15,285 per annum, 2020/21 rate) and research/training expenses (£1,000 per annum). EPSRC DTP studentships are open to both Home and International students; however, in line with guidance from UK Research and Innovation (UKRI), the number of awards available to International candidates will be limited to 30% of the total. We advise checking our funding webpages before applying: https://www.bath.ac.uk/corporate-information/funding-for-doctoral-research-in-science/ = Projects and Supervisors = VERIFICATION FOR REAL POLYNOMIAL ARITHMETIC Russell Bradford | r.j.bradf...@bath.ac.uk | http://people.bath.ac.uk/masrjb/ James Davenport | j.h.davenp...@bath.ac.uk | http://people.bath.ac.uk/masjhd/ Many problems in building verified software systems in the real world (e.g. air traffic control) involve the proof of statements about real polynomial arithmetic, often including inequalities. In principle we have known how to solve such systems for many years, but the theoretical, and too often the practical, complexity is excessive. There has been much work, at Bath, Coventry and elsewhere, in reducing the cost for important special cases, notably the cases when there are equations as well as inequalities. However, this leads to a large piece of software, resting on fairly complicated theorems. Recent research by Bath, Coventry and RWTH has produced a method (http://arxiv.org/abs/2004.04034) which converts such a problem into a sequence of simpler statements, which may be much
[TYPES/announce] PhD in Mathematical Foundations in Bath - deadline 21 Feb
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are recruiting for 2 PhD positions Funding: Competition funded Deadline: Sunday 21 February 2021 Start:October 2021 (anticipated) Mathematical Foundations Group Department of Computer Science University of Bath = The Mathematical Foundations group = Our group explores some of the deepest topics in logic and their relation to the theory of computation. We establish bridges between proof theory, category theory, semantics and complexity, so that the methods of each discipline enrich the others. We design new theories and solve old problems. For example, we defined a new proof formalism, called 'open deduction', that allowed us to describe one of the most efficient known notions of computation for the lambda-calculus. That was made possible by introducing ideas from complexity theory and category theory into proof theory and its computational interpretations. Our research programme, in a nutshell, is to help develop the mathematics of computation. This matters at least for two reasons. The first is that computing, at present, is art, not engineering. Indeed, because of the lack of mathematics, software correctness is not guaranteed the same way a bridge is guaranteed to stand, for example. The second reason is that the theory of computation is rapidly becoming one of the most important intellectual achievements of civilisation. For example, it is now helping physics and biology create new models in their domain. Because of all that, our doctoral graduates have embarked on excellent academic careers in some of the most intellectually rewarding and innovative branches of research, and will continue to do so. Our webpage: https://www.bath.ac.uk/projects/mathematical-foundations-of-computation/ Please see at the end of this email for a list of projects and supervisors. = Contact = For questions about the project or the application process, please contact us, Alessio Guglielmi a.guglie...@bath.ac.uk Willem Heijltjesw.b.heijlt...@bath.ac.uk or one of the supervisors of the projects at the end of this email. = How to apply = Applicants should hold, or expect to gain, a First Class or good Upper Second Class Honours degree in Mathematics or Computer Science, or the equivalent from an overseas university. A Master’s level qualification would be advantageous. Formal applications should be made via the University of Bath’s online application form for a PhD in Computer Science: http://samis.bath.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app=RDUCM-FP01=0015 You would apply to a specific project and supervisor from the list at the end of this email. More information on the general applications process is here: http://www.bath.ac.uk/guides/how-to-apply-for-doctoral-study/ Non-UK applicants will also be required to have met the English language entry requirements of the University of Bath: http://www.bath.ac.uk/corporate-information/postgraduate-english-language-requirements-for-international-students/ Anticipated start date: Monday 4 October 2021 = Funding = Candidates applying for this project may be considered for a 3.5-year studentship from the Engineering and Physical Sciences Council (EPSRC DTP). Funding covers tuition fees, a stipend (£15,285 per annum, 2020/21 rate) and research/training expenses (£1,000 per annum). EPSRC DTP studentships are open to both Home and International students; however, in line with guidance from UK Research and Innovation (UKRI), the number of awards available to International candidates will be limited to 30% of the total. We advise checking our funding webpages before applying: https://www.bath.ac.uk/corporate-information/funding-for-doctoral-research-in-science/ = Projects and Supervisors = VERIFICATION FOR REAL POLYNOMIAL ARITHMETIC Russell Bradford | r.j.bradf...@bath.ac.uk | http://people.bath.ac.uk/masrjb/ James Davenport | j.h.davenp...@bath.ac.uk | http://people.bath.ac.uk/masjhd/ Many problems in building verified software systems in the real world (e.g. air traffic control) involve the proof of statements about real polynomial arithmetic, often including inequalities. In principle we have known how to solve such systems for many years, but the theoretical, and too often the practical, complexity is excessive. There has been much work, at Bath, Coventry and elsewhere, in reducing the cost for important special cases, notably the cases when there are equations as well as inequalities. However, this leads to a large piece of software, resting on fairly complicated theorems. Recent research by Bath, Coventry and RWTH has produced a method (http://arxiv.org/abs/2004.04034) which converts such a problem into a sequence of simpler statements, which may be much
[TYPES/announce] 6-Month postdoc in lambda-calculi and effects, University of Bath
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We invite applications for a post-doctoral research position, to investigate a new approach to efficient computation with and without computational effects in the lambda-calculus. This is a 6-month fixed-term role starting as soon as possible. It is part of the EPSRC-funded project `Typed Lambda-Calculi with Sharing and Unsharing'. To apply: http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=CC8432 Enquiries: w.b.heijlt...@bath.ac.uk Deadline: 27 July 2021 The project revolves around new ideas in lambda-calculus and functional programming, focused in two areas. The first is *computational effects*, where the project has developed a simple and natural approach that subsumes many existing efforts, called the Functional Machine Calculus (FMC). The second is *efficient computation*, which combines ideas from proof theory and optimal reduction to investigate new, refined type systems for the lambda-calculus. The background and the source of original ideas is a branch of proof theory called "deep inference", which is closely related to category theory. Knowledge of this area is not essential to the advertised role. We are looking for excellent candidates with a PhD (or expected to complete one soon) and a proven track record in one or more of the following areas: * Lambda-calculus * Functional programming theory * Computational effects * Semantics of programming * Deep-inference proof theory As the successful candidate, you would contribute to one of several potential tasks, for example: * expanding the FMC to a prototype functional language * investigating new type systems for the FMC * investigating efficient implementations of the FMC * further develop type systems towards optimal reduction You will be part of the Mathematical Foundations group in the Department of Computer Science. We are a small, lively research group with an excellent international reputation. Some of our members are: Alessio Guglielmi http://alessio.guglielmi.name Willem Heijltjes http://willem.heijltj.es Jim Laird http://researchportal.bath.ac.uk/en/persons/james-laird Guy McCusker http://researchportal.bath.ac.uk/en/persons/guy-mccusker Thomas Powell http://t-powell.github.io Present circumstances permitting, you will have the opportunity to travel to various collaborators on the project in Europe, for example in Bologna and Paris. The University of Bath is a top-ranking university and a great place to work. Bath is a Unesco World Heritage city with fantastic amenities offering excellent quality of life. Links: Job advert: http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=CC8432 Typed Lambda-Calculi with Sharing and Unsharing: http://willem.heijltj.es/Unsharing Mathematical Foundations Group: http://www.bath.ac.uk/projects/mathematical-foundations-of-computation/ Department of Computer Science: http://www.bath.ac.uk/departments/department-of-computer-science/
[TYPES/announce] PhD positions in Mathematical Foundations of Computer Science - Bath - deadline 4 March
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are recruiting for 2 PhD positions Funding: Competition funded Deadline: Friday 4 March 2022 Start:October 2022 (anticipated) Contacts: Willem Heijltjesw.b.heijlt...@bath.ac.uk Alessio Guglielmi a.guglie...@bath.ac.uk Mathematical Foundations Group Department of Computer Science University of Bath = The Mathematical Foundations group = Our group explores some of the deepest topics in logic and their relation to the theory of computation. We establish bridges between proof theory, category theory, semantics and complexity, so that the methods of each discipline enrich the others. We design new theories and solve old problems. For example, we defined a new proof formalism, called 'open deduction', that allowed us to describe one of the most efficient known notions of computation for the lambda-calculus. That was made possible by introducing ideas from complexity theory and category theory into proof theory and its computational interpretations. Our research programme, in a nutshell, is to help develop the mathematics of computation. This matters at least for two reasons. The first is that computing, at present, is art, not engineering. Indeed, because of the lack of mathematics, software correctness is not guaranteed the same way a bridge is guaranteed to stand, for example. The second reason is that the theory of computation is rapidly becoming one of the most important intellectual achievements of civilisation. For example, it is now helping physics and biology create new models in their domain. Because of all that, our doctoral graduates have embarked on excellent academic careers in some of the most intellectually rewarding and innovative branches of research, and will continue to do so. Our webpage: https://urldefense.com/v3/__https://www.bath.ac.uk/projects/mathematical-foundations-of-computation/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3tywO-43g$ Please see at the end of this email for a list of projects and supervisors. = How to apply = To apply, please send a CV and transcript to one of the contacts: Willem Heijltjesw.b.heijlt...@bath.ac.uk Alessio Guglielmi a.guglie...@bath.ac.uk We recommended to contact us informally first, or to contact one of the supervisors of the projects at the end of this email. Please use the above contacts also for any questions. Applicants should hold, or expect to gain, a First Class or good Upper Second Class Honours degree in Mathematics or Computer Science, or the equivalent from an overseas university. A Master’s level qualification would be advantageous. Non-UK applicants will also be required to have met the English language entry requirements of the University of Bath: https://urldefense.com/v3/__http://www.bath.ac.uk/corporate-information/postgraduate-english-language-requirements-for-international-students/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3sA8_Jw0A$ Anticipated start date: Monday 3 October 2022 = Funding = Candidates applying for this project may be considered for a 3.5-year studentship from the Engineering and Physical Sciences Council (EPSRC DTP). Funding covers tuition fees, a stipend (£15,609 per annum, 2021/22 rate) and research/training expenses (£1,000 per annum). EPSRC DTP studentships are open to Home students, and a limited number of opportunities are available to excellent International candidates. = Projects and Supervisors = VERIFICATION FOR REAL POLYNOMIAL ARITHMETIC Russell Bradford | r.j.bradf...@bath.ac.uk | https://urldefense.com/v3/__http://people.bath.ac.uk/masrjb/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3uOsAYPAA$ James Davenport | j.h.davenp...@bath.ac.uk | https://urldefense.com/v3/__http://people.bath.ac.uk/masjhd/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3vY7opZDA$ Tom Powell| trj...@bath.ac.uk | https://urldefense.com/v3/__http://t-powell.github.io__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3spNE1KdA$ Many problems in building verified software systems in the real world (e.g. air traffic control) involve the proof of statements about real polynomial arithmetic, often including inequalities. In principle we have known how to solve such systems for many years, but the theoretical, and too often the practical, complexity is excessive. There has been much work, at Bath, Coventry and elsewhere, in reducing the cost for important special cases, notably the cases when there are equations as well as inequalities. However, this leads to a large piece of software, resting on fairly complicated theorems. Recent
[TYPES/announce] PhD positions in Mathematical Foundations of Computer Science, Bath - deadline 16 May
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are recruiting for 2 PhD positions Funding: Competition funded Deadline: Monday 16 May 2022 Start:October 2022 (anticipated) Contacts: Willem Heijltjesw.b.heijlt...@bath.ac.uk Alessio Guglielmi a.guglie...@bath.ac.uk Mathematical Foundations Group Department of Computer Science University of Bath = The Mathematical Foundations group = Our group explores some of the deepest topics in logic and their relation to the theory of computation. We establish bridges between proof theory, category theory, semantics and complexity, so that the methods of each discipline enrich the others. We design new theories and solve old problems. For example, we defined a new proof formalism, called 'open deduction', that allowed us to describe one of the most efficient known notions of computation for the lambda-calculus. That was made possible by introducing ideas from complexity theory and category theory into proof theory and its computational interpretations. Our research programme, in a nutshell, is to help develop the mathematics of computation. This matters at least for two reasons. The first is that computing, at present, is art, not engineering. Indeed, because of the lack of mathematics, software correctness is not guaranteed the same way a bridge is guaranteed to stand, for example. The second reason is that the theory of computation is rapidly becoming one of the most important intellectual achievements of civilisation. For example, it is now helping physics and biology create new models in their domain. Because of all that, our doctoral graduates have embarked on excellent academic careers in some of the most intellectually rewarding and innovative branches of research, and will continue to do so. Our webpage: https://urldefense.com/v3/__https://www.bath.ac.uk/research-groups/mathematical-foundations-of-computation/__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20Nectr4_$ Please see at the end of this email for a list of projects and supervisors. = How to apply = To apply, please complete the following online form: https://urldefense.com/v3/__https://samis.bath.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app=RDUCM-FP01=0016__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20MasVTIB$ Applicants should hold, or expect to gain, a First Class or good Upper Second Class Honours degree in Mathematics or Computer Science, or the equivalent from an overseas university. A Master’s level qualification would be advantageous. Non-UK applicants will also be required to have met the English language entry requirements of the University of Bath: https://urldefense.com/v3/__http://www.bath.ac.uk/corporate-information/postgraduate-english-language-requirements-for-international-students/__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20Lx3hym9$ Anticipated start date: Monday 3 October 2022 = Funding = Candidates applying for this project may be considered for a 3.5-year studentship from the Engineering and Physical Sciences Council (EPSRC DTP). Funding covers tuition fees, a stipend (£15,609 per annum, 2021/22 rate) and research/training expenses (£1,000 per annum). EPSRC DTP studentships are open to Home students, and a limited number of opportunities are available to excellent International candidates. = Projects and Supervisors = VERIFICATION FOR REAL POLYNOMIAL ARITHMETIC Russell Bradford | r.j.bradf...@bath.ac.uk | https://urldefense.com/v3/__http://people.bath.ac.uk/masrjb/__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20BOBjs4C$ James Davenport | j.h.davenp...@bath.ac.uk | https://urldefense.com/v3/__http://people.bath.ac.uk/masjhd/__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20Akrtr7S$ Tom Powell| trj...@bath.ac.uk | https://urldefense.com/v3/__http://t-powell.github.io__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20EvuXGzT$ Many problems in building verified software systems in the real world (e.g. air traffic control) involve the proof of statements about real polynomial arithmetic, often including inequalities. In principle we have known how to solve such systems for many years, but the theoretical, and too often the practical, complexity is excessive. There has been much work, at Bath, Coventry and elsewhere, in reducing the cost for important special cases, notably the cases when there are equations as well as inequalities. However
