Faculty positions at the Department of Computer Science, Reykjavik University

This job ad could be of interest to you or to someone you know. Feel free to spread it as you see fit. Thanks!

 

The Department of Computer Science at Reykjavik University invites applications for several full-time faculty positions.

We are looking for energetic, highly qualified academics who are eager to develop their own research programs, strengthen existing research within the department and build bridges with industry. Of particular interest are candidates in the areas of machine learning, data science, computer security and software systems, broadly construed, but exceptionally qualified candidates from all areas of computer science are encouraged to apply.

Candidates should have a proven international research record that is commensurate with the level of the position for which they apply. The successful applicants will play a full part in the teaching and administrative activities of the department; in particular, they will teach courses and supervise students at both graduate and undergraduate level. Applicants having a demonstrated history of excellence in teaching are preferred. A PhD in computer science or a related field is required.

Salary and rank are commensurate with experience. An appointment at assistant-professor level is permanent track, with the expectation that a successful candidate will qualify for promotion to associate professor within six years.

The positions are open until filled, with the earliest available starting date in August 2020. Later starting dates can be negotiated.

The review of the applications will begin on Monday, 17 February 2020, and will continue until the positions are filled.

See http://radningar.hr.is/storf/viewjobonweb.aspx?jobid=3558 for further information on how to apply for the position and on the required documents.

About the department, Reykjavik University and Iceland

The Department of Computer Science at Reykjavik University has about 650 full-time-equivalent students and 22 faculty members. It provides an excellent working environment that encourages and supports independence in academic endeavours, and in which a motivated academic can have impact at all levels. The department offers undergraduate and graduate programs in computer science and software engineering, as well as a combined-degree undergraduate program in discrete mathematics and computer science. The doctoral program within the department received its ministerial accreditation in 2009 and has been active ever since.

The department is home to several research centres producing high-quality collaborative research in areas such as artificial intelligence, financial technology, language technology, software systems, and theoretical computer science, among others; for more information on those research centres, see https://en.ru.is/research/units/.

On the Times Higher Education rankings for 2020, Reykjavík University is ranked in first place along with six other universities for the average number of citations per faculty. Overall, according to that list, RU is ranked among the 300 best universities world-wide, 52nd out of all universities established fewer than 50 years ago, 14th among universities with fewer than 5000 students, and first among Icelandic universities.

Iceland is well known for its breathtaking natural beauty, with volcanoes, geysers, hot springs, lava fields and glaciers offering a dramatic landscape. It is consistently ranked as one of the best places in the world to live. It offers a high quality of life, is one of the safest places in the world, has high gender equality, and strong health-care and social-support systems. It is in fourth position in the 2019 UN World Happiness Report, which ranks the world's countries by their happiness level.

For further information about the Department of Computer Science at Reykjavik University and its activities, see http://en.ru.is/scs/.

Call for opinions: Length of papes in conference proceedings in TCS

As current chair of the editorial board of LIPIcs, Leibniz International Proceedings in Informatics, I have been looking at some data about the length of the papers published in the series. The average length of the articles published in LIPIcs in 2019 so far is of 15.8 pages, including front matter and bibliography. However, three of the published papers are over 40 pages and three conferences have an average article length above 20 pages (22, 23.9 and 28.4, respectively).

I have seen that some conferences in TCS have no limit on the length of the submitted papers. A colleague whose opinions I hold in high esteem wrote to me saying:

Some people in the "conference name removed" community strongly feel there should be no page limit. My opinion may not be as strong as some, but I believe these people have a point.

Whether we like it or not, most papers in the TOC community only appear in conferences. Many of those conferences have no page limit for submissions, and encourage authors to include all proofs while making sure that the key ideas are presented in the first 10 pages or so. Scientific progress is hindered when authors are then forced to take out parts of their writeups for the conference proceedings in order for their papers to fit within the page limits. One may wish that they'd publish a full version of their paper in a journal subsequently, but most of them won't bother. The net effect is that there is no actual paper with all the details, which is no good.

I share the point made in the last sentence, but I am somewhat bothered by the fact that full versions of papers in TCS are increasingly not being submitted to journals. I am probably very old fashioned, but I feel that it is desirable to see our published results vetted by a journal-strength review process. I still view conferences as means for the rapid dissemination of results and as a meeting point for their community of reference, and I consider journals as the media for final archival publication of mature pieces of research. However, with my LIPIcs EB chair hat on and out of personal interest, I am keen to hear your opinion on whether it is good for the TCS community to publish only in conferences and to publish conference papers without page limits, bearing in mind that, quoting from the FOCS 2019 call for papers:

Although there is no bound on the length of a submission, material other than the title page, references, and the first ten pages will be read at the committee’s discretion.

I'd be grateful if you could post your thoughts on this matter in the comment section. Let's focus on what is best for the dissemination of science, even though long articles are more expensive than those whose average length is around 15 pages.

I look forward to hearing your opinions. Thanks in advance!

Facebook Testing and Verification Research Award to two CS@GSSI students

It gives me great pleasure to inform you that the project "Static prediction of test flakiness" submitted by Breno Alexandro Ferreira de Miranda (Federal University of Pernambuco, Brazil), Antonia Bertolino (Istituto di Scienza e Tecnologie dell’Informazione – CNR), Emilio Cruciani (Gran Sasso Science Institute) and Roberto Verdecchia (Gran Sasso Science Institute) has been selected for a Facebook Testing and Verification research award. Congratulations to everyone and to CS@GSSI as a whole!

The winners have been selected from a pool of over 100 proposals and are listed at 

https://research.fb.com/blog/2019/10/announcing-the-winners-of-the-2019-testing-and-verification-research-awards/. 

Quoting from that web page: 

“We are excited that, once again, we received over 100 proposals, and of such high quality,” says Mark Harman, Research Scientist and Facebook TAV co-chair. “We are really excited to see this research develop, and to see the deployment of advanced research in industry.

“Despite doubling the funding available this year, there were many excellent proposals that we were sadly unable to fund this round. Such was the quality of the proposals we received,” says Mark. “We are very grateful to the scientific research community for engaging so enthusiastically with this call for proposals.”

The award will be presented at the upcoming Facebook Testing and Verification Symposium.

PhD position at TU/e on product line engineering in multidisciplinary cyber-physical systems

The Model Driven Software Engineering section at Eindhoven University of Technology (TU/e) is searching for a candidate for a fully-funded PhD position on product line engineering in the multidisciplinary context of cyber-physical systems to collaborate with the high-tech company ASML in the context of the EU ECSEL project Arrowhead Tools.

See here for the details of the position.

TU/e is a dynamic, research-intensive university in the heart of Europe, and in the Brainport region, a leading European technology region, and a centre for innovation and hi-tech industry. TU/e is consistently ranked within the top-100 positions in several world rankings for its research and quality of education.

Two PhD positions at the Department of Computer Science Reykjavik University

My Reykjavik colleagues Anna Sigríður Íslind and María Óskarsdóttir have two PhD positions available at Reykjavik University, Iceland. The position announcements are below. Please contact them for more information. In my biased opinion, they will be excellent PhD supervisors.

-----------------------------------------------------------------------------------------------------

Position 1: PhD position in learning analytics and informatics

Information about the research topic

We are looking for a full-time PhD student to conduct research on learning analytics in the context of learning management platforms. The aim of the PhD position is to study learning behavior in higher education through learning management platforms which are widely used for administration, documentation and reporting of educational courses and learning programs. The behavioral data that is generated while students use the platforms can be analyzed to understand how they interact with the learning content in relation to the learning outcomes and objectives. The PhD candidate will study learning behavior using advanced analytics and machine learning techniques with the goal of discovering patterns in learning as well as to understand and optimize the learning process and the environment in which it occurs, as well as investigate how the architecture of the learning environment enables learning.

Information about the department and the university

You will join us at the Department of Computer Science, Reykjavík University. The department covers a broad range of research topics in Computer Science and is engaged in several national and international research projects, often interdisciplinary in nature.

Reykjavík University is a private university located in Reykjavík, Iceland. The university currently hosts approximately 3500 students, divided into the Departments of Computer Science, Sport Science, Psychology, Business, Law, Applied Engineering, and Engineering. All of Reykjavík University is located in a single building in one of the most beautiful areas of Reykjavík.

Qualification requirements

Candidates should have a strong interest in data science, information systems research as well as learning and teaching. To be eligible for this position, you should have/be about to obtain an MSc degree in Computer Science, Statistics, Information Systems, Informatics, Mathematics, Engineering or related fields. Strong candidates with a background in other relevant topics are very much encouraged to apply as well.

Position summary

Full-time temporary employment (currently paid 365,000 ISK per month before taxes, roughly 3000 USD at current exchange rate). You are expected to finish your PhD within four years' time. The position includes teaching duties of roughly 20%.

Application procedure

Interested applicants should submit their application through the recruitment website radningar.hr.is

The application should include

• CV 
• Research proposal stating the possible development of what you would like to do based on the description above (ca. 2 pages)
• Two letters of reference (e.g., from academic supervisors, former superiors)
• A 1 to 3-page personal letter where you introduce yourself and present your qualifications/experience/interests
• Attested copies of education certificates, including grade reports
• Bachelor and/or Master thesis
• Research publications, if existent
• Links to software repositories with relevant projects, if existent

-------------------------------------------------------------------------------------------

Position 2: PhD position in informatics focusing on health platforms

Information about the research topic

We are looking for a full-time PhD student to conduct research on design, development and use of platforms for continuous data gathering for health purposes. The aim of the PhD position is to study the design and development of a health data platform that takes in health data and how the health data can be used for decision-making purposes. The cases more specifically both includes data from extremely healthy individuals (on elite sport level) and on the other hand, from those that are chronically ill. The focus in the beginning will be on data from national teams collected both through measurements during practice, and on continuous data collection through wearable technologies. The PhD student will study the design and development of the multi-sided platform and how the use of the platform effects different stakeholders involved. For instance, the data collected by athletes, can be used by them as well as by trainers and researchers, which has implications both for the design process, as well as for those using the data. In addition, the PhD student will also study a case of chronically ill individuals, where the data is from the same types of technologies, but can be used for a different purpose, to support decision-making processes in healthcare. In these cases the where the stakeholders are patients , that gather data that which can be used by medical staff to support their decision-making process, and by researchers. Furthermore, we will apply machine learning and advanced analytics to discover patterns that can on the one hand help athletes enhance their performance and on the other hand detect warning signs for the chronically ill. In addition, on the topic of learning from data and designing, and developing platforms for health and wellbeing purposes, the PhD student will also work with a case on new ways of screening for breast cancer.

Information about the department and the university

You will join us at the Department of Computer Science, Reykjavík University. The department covers a broad range of research topics in Computer Science and information systems and is engaged in several national and international research projects, often interdisciplinary in nature.

Reykjavík University is a private university located in Reykjavík, Iceland. The university currently hosts approximately 3500 students, divided into the Departments of Computer Science, Sport Science, Psychology, Business, Law, Applied Engineering, and Engineering. All of Reykjavík University is located in a single building in one of the most beautiful areas of Reykjavík. Reykjavík University is a private university located in Reykjavík, Iceland. The university currently hosts approximately 3500 students, divided into the Schools of Computer Science, Business, Law, and Science and Engineering. All of Reykjavík University is located in a single building in one of the most beautiful areas of Reykjavík.

Qualification requirements

Candidates should have a strong interest in data science, information systems research as well as in wellbeing and health related topics. To be eligible for this position, you should have/be about to obtain an MSc degree in Computer Science, Information Systems, Informatics, Engineering or related fields. Strong candidates with a background in other relevant topics are very much encouraged to apply as well.

Position summary

Full-time temporary employment (currently paid 365,000 ISK per month before taxes, roughly 3000 USD at current exchange rate). You are expected to finish your PhD within four years' time. The position includes teaching duties of roughly 20%.

Application procedure

Interested applicants should submit their application through the recruitment website; radningar.hr.is
The application should include:

• CV 
• Research proposal stating possible development that extends what you would like to do, based on the description above (ca. 2 pages)
• Two letters of reference (e.g., from academic supervisors, former bosses/superiors)
• A 1 to 3-page personal letter where you introduce yourself and present your qualifications/experience/interests
• Attested copies of education certificates, including grade reports
• Bachelor and/or Master thesis.
• Research publications, if existent
• Links to software repositories with relevant projects, if existent

The deadline for application in November 1st, 2019. We will start reviewing applications as soon as they arrive. We strongly encourage interested applicants to send their applications as soon as possible.

Questions?

If you have any questions, want more details on the position, or just check before sending in your application, please contact us directly!

Anna Sigríður Íslind

Assistant Professor | School Department of Computer Science, Reykjavík University

annasi@ru.is

María Óskarsdóttir 

Assistant Professor | School Department of Computer Science, Reykjavík University

mariaoskars@ru.is

PhD position at TU Wirn: Formal methods applied to the specification and monitoring of large-scale, spatially-distributed, stochastic systems

Interesting PhD position at TU Wien with Ezio Bartocci and Laura Nenzi. Spread the news! 

The Institute of Computer Engineering at the Technische Universität Wien (TU Wien) is seeking a candidate for a research assistant position (PhD student, 4 years). The position is available from September (a starting date until Fall 2019 is intended) and the successful candidate will be a PhD student of the LogiCS Doctoral Program and she/he will be supervised by Prof. Ezio Bartocci <http://www.eziobartocci.com/> and co-supervised by Dr. Laura Nenzi <https://lauranenzi.github.io/>
The successful applicant will carry out his/her PhD in the research area of formal methods applied to the specification and monitoring of large-scale, spatially-distributed, stochastic systems.
The position in funded by the ÖAW and the FWF <https://m.fwf.ac.at/en/research-funding/personnel-costs/> for the recently acquired YIRG grant: “High-dimensional statistical learning: new methods to advance economic and sustainability policies”, an interdisciplinary project to be led for the TU part by PhD Laura Nenzi.
TASK DESCRIPTION (leader Laura Nenzi):
Formal methods provide precise formal specification languages that can be easily interpreted by humans and verification algorithms that can check in an automatic way the value of satisfaction of interesting properties. One of the main problems of such techniques is the curse of dimensionality. A possibility to treat the problem is to use approximate methods such as statistical model checking. However, even these methodologies can be unfeasible for very-large-scale stochastic systems. A new research line consists of exploiting machine learning techniques and Bayesian inference to identify relevant data and decrease the computational cost, permitting the application of such powerful formal analysis on very complex systems. An important aspect that will be covered in the study is the spatial configuration of such systems, a key feature in several real case studies that are considering in the project. The methodology will be principally applied to tackle questions related to sustainable urban mobility and thus responsible consumption.
APPLICATION
Please apply your application following the instructions in the DK LogiCS admission portal. https://logic-cs.at/phd/admission/ <https://logic-cs.at/phd/admission/>, by indicating in the application form: Prof. Ezio Bartocci and Dr. Laura Nenzi as supervisors. While it is not necessary to have the Master degree at the moment of the application, it is instead mandatory to complete it before starting the PhD.
CONTACT DETAILS
For further information and inquiries about this post please contact Laura Nenzi, e-mail: laura.nenzi@gmail.com .

Postdoc position at the GSSI in algorithms for modern networks, formal methods for reactive systems and model-based software engineering

Postdoctoral position financed by the GSSI

Scientific profile: The successful candidate will have a strong research record in one or more of the research areas within the Computer Science group at the GSSI, namely algorithms for modern networks, formal methods for reactive systems and model-based software engineering. We welcome applications in any of those areas.

The position is for two years (renewable for a third year, if this is mutually agreeable) and the salary is 36,000€ per year before taxes.

How to apply: The application must be submitted through the online form available at https://applications.gssi.it/postdoc/ by Thursday, 11 July 2019 at 6 p.m. (Central European Time). For more information, please consult the Call for Applications at https://applications.gssi.it/postdoc/.

Requirements: Candidates are expected to have a PhD degree in Computer Science or related disciplines.

Postdoctoral position at the GSSI within the project “ALGADIMAR: Algorithms, Games, and Digital Markets”

The Computer Science group at the Gran Sasso Science Institute (GSSI, http://cs.gssi.it) --- an international PhD school and centre for advanced studies located in L’Aquila, Italy --- has one available postdoctoral position  in the context of the PRIN projects  “ALGADIMAR: Algorithms, Games, and Digital Markets” (Gianlorenzo D’Angelo, PI at GSSI), funded by the Italian Ministry for University and Research.

The position is briefly described below. It is for two years and the salary is 36,000€ per year before taxes. The position is renewable for a third year, if this is mutually agreeable.

How to apply: The application must be submitted through the online form available at https://applications.gssi.it/postdoc/ by Thursday, 11 July 2019 at 6 p.m. (Central European Time). For more information, please consult the Call for Applications at https://applications.gssi.it/postdoc/ or write an email to Gianlorenzo D’Angelo.

Requirements: Candidates are expected to have a PhD degree in Computer Science or related disciplines. Preference will be given to applicants who have previous research experience on topics related to the theme of the project.

Postdoctoral position within the project “ALGADIMAR: Algorithms, Games, and Digital Markets”, supervised by Gianlorenzo D’Angelo. 

Brief description of the project: Digital markets form an increasingly important component of the global economy. The Internet has enabled new markets with previously unknown features (e-commerce, web-based advertisement, viral marketing, sharing economy, real-time trading), and algorithms play a central role in many decision processes involved in these markets. For example, algorithms run electronic auctions, adjust prices dynamically, trade stocks, harvest big data to decide market strategies and to provide recommendations to customers. The focus of the proposal ALGADIMAR is on the development of new methods and tools in research areas that are critical to the understanding of digital markets: algorithmic game theory, market and mechanism design, machine learning, algorithmic data analysis, optimization in strategic settings. We plan to apply these methods so as to solve fundamental algorithmic problems motivated by Internet advertisement, sharing economy, mechanism design for social good, security games. While our research is focused on foundational work —with rigorous design and analysis of algorithms, mechanisms and games— it will also include empirical validation on large-scale datasets from real-world applications.

Main activities: The research activity will be on one or more of the following topics: design and analysis of algorithms; algorithms and data structures for big data; approximation algorithms; combinatorial optimization; algorithms for graphs and networks; autonomous agents and mobile computing; distributed algorithms; algorithmic game theory, algorithmic aspects of internet and social networks.

Postdoctoral positions at the GSSI on modelling and verification for cyber-physical and smart systems

The Computer Science group at the Gran Sasso Science Institute (GSSI, an international PhD school and centre for advanced studies located in L’Aquila, Italy) has two available postdoctoral positions on topics related to modelling and verification for cyber-physical and smart systems. The positions are in the context of two PRIN projects funded by the Italian Ministry for University and Research, namely "Designing Spatially Distributed Cyber-Physical Systems under Uncertainty (SEDUCE)" (Catia Trubiani, PI at the GSSI) and "IT MATTERS: Methods and Tools for Trustworthy Smart Systems" (Luca Aceto, PI at the GSSI). Each position is for two years and the salary is 36,000€ per year before taxes. The positions are renewable for a third year if this is mutually agreeable.

The positions are briefly described below. We foresee a close collaboration between the members of the teams working on the two projects. The application must be submitted through the online form available at https://applications.gssi.it/postdoc/ by Thursday, 11 July 2019 at 6 p.m. (Central European Time). For more information, please consult the Call for Applications at https://applications.gssi.it/postdoc/ or write an email to the PIs of the respective projects.

Note that the Computer Science group at the GSSI also has a further position financed by the institute, which can be filled in any of the research themes within the group. See http://cs.gssi.it for more information.

Requirements: Candidates are expected to have a PhD degree in Computer Science or related disciplines. Preference will be given to applicants who have previous research experience on topics related to the themes of the project.

Postdoctoral position within the project "Designing Spatially Distributed Cyber-Physical Systems under Uncertainty", supervised by Catia Trubiani: https://cs.gssi.it/catia.trubiani.

Brief description of the project: Emerging scenarios such as autonomous vehicles and the Internet-of-Things require large-scale cyber-physical systems (CPS), i.e., computing devices that interact with the physical world. To cope with their complexity, model-based design has long been advocated as a prominent approach for their rigorous development. However, the state of the art does not adequately account for two major issues: space, to capture the distribution of CPS devices as well as their mobility; and uncertainty, e.g., to reflect lack of knowledge about the environment, the accuracy of the model, or errors occurring in the real world. Our goal is to develop modelling and analysis techniques for CPS where space and uncertainty are first-class citizens. We envisage a component-based framework where digital and physical components have locality and mobility features, and where uncertainty is captured by means of probabilistically distributed activities to describe their dynamics. We devise a system to specify spatio-temporal CPS requirements, turning them into probabilistic spatio-temporal logical specifications that will be at the basis of efficient algorithms for the analysis, verification, and synthesis. We will apply our techniques to real case studies on smart buildings and crowd-navigating robots.

Main activities: The successful candidate will develop a component-based modelling language for the specification of cyber physical systems, where digital components (i.e., the computational devices), need to co-exist with physical components (i.e., the dynamical models of the physical world). Each component will feature an appropriate location and mobility model. Uncertainty will be specified with either probabilistically distributed activities, or nondeterministically, leading to reasoning that will take into account worst- and best-case scenarios under any possible value of such uncertain actions. The modelling framework will allow the specification of spatio-temporal requirements, which establish the behavioural guarantees to be satisfied by the CPS under analysis. The postdoctoral researcher will work with Catia Trubiani at the GSSI, and she/he will also collaborate with the project partners at IMT Lucca (Mirco Tribastone, coordinator of the project), University of Trieste (Luca Bortolussi and Stefano Seriani), and University of Camerino (Francesco Tiezzi).


Postdoctoral position within the project "IT MATTERS: Methods and Tools for Trustworthy Smart Systems" supervised by Luca Aceto: http://www.gssi.it/people/professors/lectures-computer-science/item/225-aceto-luca.

Brief description of the project: The goal of the project is the development and the application of a novel methodology for the specification, implementation and validation of trustworthy smart systems based on formal methods. We envisage system development in three steps by first providing and analysing system models to find design errors, then moving from models to executable code by translation into domain-specific programming languages and, finally, monitoring runtime execution to detect anomalous behaviours and to support systems in taking context-dependent decisions autonomously. Scientifically, the research will yield new, fundamental insights on the general properties of large scale, physically located, smart systems, leading to an end-to-end, principled approach to their design, implementation and deployment. The developed software tools and the work on the case studies will show the effectiveness of our proposed approach in three practical scenarios at different application scales.

Main activities: The successful candidate will develop runtime-monitoring and software-model-checking techniques for “smart systems”, that is, systems that take context-dependent decisions autonomously. The research activities will involve developing frameworks that can deal with the distributed nature of smart systems and will build on existing work on specification-based monitoring and software model checking of cyber-physical systems. The postdoctoral researcher will also devise techniques to use information derived from the runtime analysis to guide the software-model-checking effort and to refine the models of the runtime environment used in model checking. The postdoctoral researcher will work with Luca Aceto, Omar Inverso, Ludovico Iovino and Emilio Tuosto at the GSSI. He/she will also collaborate with the project partners at IMT Lucca, CNR Pisa, University of Camerino, University of Pisa and University of Udine. Moreover, he/she will also interact with the concurrency group at ICE-TCS (http://icetcs.ru.is/), Reykjavik University, led by Luca Aceto and Anna Ingólfsdóttir.

An interview with Jamie Gabbay and Andrew Pitts, 2019 Alonzo Church Award recipients

The 2019 Alonzo Church Award committee consisting of Thomas Eiter, Javier Esparza, Radha Jagadeesan, Catuscia Palamidessi, and Natarajan Shankar, have selected Murdoch J. Gabbay and Andrew M. Pitts for the 2019 Alonzo Church Award, for introducing the theory of nominal representations, a powerful and elegant mathematical model for computing with data involving atomic names. In particular, the nomination for the Alonzo Church Award singled out the following two papers:

• “A new approach to abstract syntax with variable binding” by Murdoch J. Gabbay and Andrew M. Pitts, Formal Aspects of Computing 13(3):341– 363, 2002; and
• “Nominal logic, a first order theory of names and binding” by Andrew M. Pitts, Information and Computation 186(2):165–193, 2003.

For the conference version of the first article, Andy and Jamie will also be receiving the Test-of-Time Award from LICS 1999.

The award recipients kindly agreed to answer some questions of mine via email. You can find the transcript of the interview below. My questions are labelled with LA, Andy's answers with AP and Jamie's with JG. I hope that you'll enjoy reading their insights and the story of their award-receiving work as much as I did myself.

LA: You are receiving the 2019 Alonzo Church Award for Outstanding Contributions to Logic and Computation as well as the Test-of-Time Award from LICS 1999 for your invention of nominal techniques to provide a semantic understanding of abstract syntax with binding.   Could you briefly describe the history of the ideas that led you to use the permutation model of set theory with atoms due to Fraenkel and Mostowski to represent name abstraction and fresh name generation? What were the main inspirations and motivations for your work? In your opinion, how did nominal techniques advance the state of the art at that time?

AP: I have had a long-standing interest in the mathematical semantics of programming language features that restrict resources to a specific scope, or hide information from a program's environment; think local mutable state in languages like OCaml, or channel-name restriction in the pi-calculus. When Ian Stark was doing his PhD with me in the 90s we tried to understand a simple instance: the observable properties of higher-order functions combined with dynamically generated atomic names that can be tested for equality, but don't have any other attribute -- we called this the "nu-calculus". Ian gave a denotational semantics for the nu-calculus using Moggi's monad for modelling dynamic allocation. That monad is defined on the category of pullback-preserving functors from the category of injective functions between finite ordinals to the category of sets. This functor category was well-known to me from topos theory, where it is called Schanuel's topos and hosts the generic model of a geometric theory of an infinite decidable set. A few years later, when Jamie joined me as a PhD student in 1998, I suggested we look at the Schanuel topos as a setting for initial algebra semantics of syntax involving binding operations, modulo alpha-equivalence. I think Jamie prefers set theory over category theory, so he pushed us to use another known equivalent presentation of the Schanuel topos, in terms of continuous actions of the group of permutations of the set N of natural numbers (topologized as a subspace of the product of countably many copies of N). In this form there is an obvious connection with the cumulative hierarchy of sets (with atoms) that are hereditarily finitely supported with respect to the action of permuting atoms. This universe of sets was devised by Fraenkel and Mostowski in the first part of the twentieth century to model ZFA set theory without axioms of choice. Whether one emphasises set theory or category theory, the move to making permutations of names, rather than injections between sets of names, the primary concept was very fruitful. For example, it certainly makes higher-order constructions (functions and powersets) in the topos/set-theory easier to describe and use. We ended up with a generic construction for name-abstraction modulo alpha-equivalence compatible with classical higher-order logic or set theory, so long as one abstains from unrestricted use of choice.

JG: At the time it wasn't an idea to consider names as elements of a distinctive datatype of names, with properties just like other datatypes such as the natural numbers Nat. If we want to add 1 to 1, we take 1:Nat and invoke the "plus" function, which is a specific thing associated to Nat; so why not abstract a in x by assuming a:Atm (where Atm is a distinct thing in our mathematical universe) and x:X and invoking a function "abstract", which is a thing associated to Atm? We unfolded the implications of this idea in set theory and rediscovered FM sets. I was inspired by the way I saw mathematics built up in ZF set theory as an undergraduate, starting from a simple basis and building up the cumulative hierarchy. When I saw the chance to do this for a universe with names, I jumped at the chance. It turns out FM sets are not required. Nominal techniques can be built in ZFA set theory, which contains more functions and permits unrestricted choice.

LA: Over the last fifteen years, nominal techniques have become a fundamental tool for modelling locality in computation, underlying research presented in over a hundred papers, new programming languages and models of computation. They have applications to the syntax and semantics of programming languages, to logics for machine-assisted reasoning about programming-language semantics and to the automatic verification of specifications in process calculi. Variations on nominal sets are used in automata theory over infinite alphabets, with applications to querying XML and databases, and also feature in work on models of Homotopy Type Theory. When did it dawn on you that you had succeeded in finding a very good model for name abstraction and fresh name generation, and one that would have a lot of impact? Did you imagine that your model would generate such a large amount of follow-up work, leading to a whole body of work on nominal computation theory?

AP: No, to begin with I was very focussed on getting better techniques for computing and reasoning about syntax with bound names. But that only represents a part of the current broad landscape of nominal techniques, the part that mainly depends on the mathematical notion of "finite support" (a way of expressing, via name-permutation, that an object only involves finitely many names). Independently of us, some people realised that a related notion of finiteness, "orbit-finiteness" (which expresses that an object is finite modulo symmetries) is crucial for many applications of nominal techniques. I am referring to the work of Montanari and Pistore on pi-calculus and HD automata using named sets (yet another equivalent of the Schanuel topos) and the work on automata theory over infinite alphabets (and much else besides) using "sets with atoms" by the Warsaw group (Bojanczyk, Klin, Lasota, Torunczyk,...). The latter is particularly significant because it considers groups of symmetry for atoms other than the full permutation group (in which the only property of an atom preserved under symmetry is its identity).

JG: Yes, I did. Nobody could anticipate the specific applications but I knew we were on to something, which is why I stayed on to build the field after the PhD. The amount of structure was just too striking. This showed early: e.g. in the equivariance properties, and the commutation of nominal atoms-abstraction with function-spaces. When I sent the proof of this property to Andrew, at first he didn't believe it! I had a sense that there was something deep going on and I still do.

LA: What is the result of yours on nominal techniques you are most proud of? And what are your favourite results amongst those achieved by others on nominal computation?

AP: Not so much a specific result, but rather a logical concept, the freshness quantifier (which we wrote using an upside down "N" -- N stands for "New"). In informal practice when reasoning about syntax involving binders, one often chooses some fresh name for the bound variable, but then has to revise that choice in view of later ones; but fortunately any fresh name does as well as some particular one. This distinctive "some/any" property occurs all over the place when computing and reasoning about languages with binders and the freshness quantifier formalises it, in terms of the freshness ("not in the support of") relation and conventional quantifiers. For the second part of your question I would choose two things. One is the work by Jamie with Fernandez and Mackie on nominalrewriting systems, which won the PPDP Most Influential Paper 10-year Award in 2014. The second is the characterisation of orbit-finite sets with atoms in terms of "set-builder expressions"---see Klin et al, "Locally Finite Constraint Satisfaction Problems", Proc. LICS 2015); it's a nice application of the classical model theory of homogeneous structures with interesting applications for languages that compute with finite structures.

JG: Thanks for asking. Aside from the initial papers, my work on nominal rewriting with Fernandez has probably had most impact. However, I am rather fond of the thread of research going from Nominal Algebra, through the axiomatisation of substitution and first-order logic and the characterisation of quantification as a limit in nominal sets, and on to Stone duality. It's a mathematical foundation built from a nominal perspective of naming and quantification and I hope that as the state of the art in nominal techniques advances and broadens, it might prove useful. Andrew's book has been helpful in marking out nominal techniques as a field. I also agree with Andrew that orbit-finiteness and the applications of this idea to transition systems and automata, is important. I like the automata work for another concrete reason: nominal techniques were discovered in the context of names and binding in syntax, which has bequeathed a misconception that nominal techniques are only about this. The Warsaw school of nominal techniques gives an independent illustration of the other applications of these ideas.

LA: Twenty years have passed since your LICS 1999 paper and the literature on variations on nominal techniques now contains over a hundred papers. Do you expect any further development related to the theory and application of nominal techniques in the coming years? What advice would you give to a PhD student who is interested in working on topics related to nominal computation today?

AP: For the purpose of answering your question, let's agree to divide LICS topics into Programming Languages and Semantics (PLS) versus Logic and Algorithms (LAS). (So long as we don't think of it as a dichotomy!) Then it seems to me that applications of nominal techniques to LAS are currently in the ascendant and show no sign of slowing down. My own interests are with PLS and there is still work to be done there. In particular, I would like better support for using nominal techniques within the mainstream interactive theorem proving systems: we have the Nominal Package of Urban and Berghofer for classical higher-order logic within Isabelle (which lead to Urban and Tasson winning the CADE Skolem Award in 2015), but nothing analogous for systems based on dependent type theory, such as Agda, Coq and Lean. Recent work of Swan (arXiv:1702.01556) gives us a better understanding of how to develop nominal sets within constructive logic; but I have yet to see a dependent type theory that both corresponds to some form of constructive nominal logic under Curry-Howard and is sufficiently simple that it appeals to users of systems lke Coq who want to mechanise programming language meta-theory in a nameful style. Really, I would like the utility of the FreshML programming language that Jamie, Mark Shinwell and I proposed in 2003 (and which Mark implemented as a patch of OCaml) restricted to total functional programming in the style of Agda; but I don't quite know how to achieve that.

JG: Yes. We are far from understanding nominal techniques and the field has a lot of life and will continue to surprise. I've always believed that. A key sticking-point right now is implementations. I wrote a paper about this recently, on equivariance and the foundations of nominal techniques. One point in the paper is a sketch for a next-generation nominal theorem-prover (based on ZFA + equivariance). I'd like to see this carried out, so if anybody reading this is interested then please be in touch. I'd also like to see nominal techniques implemented as a package in a language like Haskell, ML, or even Python! If we can get this stuff into the working programmer's toolbox, in a way that just works and does not require special configuration, then that would be helpful. I suspect that nominal techniques as currently presented in the maths papers, might not fit into a programming language at the moment. The theory is too strong and may need weakened first. We need a subset of nominal techniques weak enough to squeeze into an existing language, yet expressive enough for interesting applications. Some general advice, specifically for the PhD student. If you have an idea which most people around you don't understand, consider this may be a gap in the collective imagination. There can be peer pressure when faced by incomprehension to blame yourself, back down, and think about something else. By all means do this, but only if you yourself judge it right to do so.

LA: Is there any general research-related lesson you have learnt in the process of working on nominal techniques?

AP: On the one hand, don't lose sight of what application your theory is supposed to be good for; but on the other hand, let beauty and simplicity be your guide.

JG: Yes:

• Proving stuff is 30% of the work; convincing people is 70%. 
• It's the basic ideas that are hard, not the complicated theorems.
• Competence and imagination are orthogonal. 
• It's doesn't have to be complex to be clever. 
• Elegant + applicable is a potent combination. 
• Seek out good listeners. Give up quickly on bad ones. Try to be a good listener. 
• Other people have a lot to teach you, but it might not be the things you expected. 
• Writing papers is fun.  

LA: Thanks to both of you for your willingness to answer my questions and congratulations for the awards you will be receiving this summer!