Interactive Theorem Proving for System Verification and Program Extraction
Lead Research Organisation:
Swansea University
Department Name: College of Science
Abstract
Key Objectives:
1. To investigate the theoretical foundation of a logic for the automatic synthesis of provably correct computer programs.
2. To develop a prototype the implements program extraction along the lines of the first objective.
The student will prove general theorems showing the correctness of extracted programs and will use advanced programming techniques (monadic effects) to implement program extraction.
The project mainly resides in the areas of Theoretical Computer Science, Logic and combinatorics,
Verification and correctness, but it also intersects substantially with Mathematical analysis (since the main applications are in analysis), Natural language processing (since the system will contain a natural language interface), Programming languages and compilers (since the operational and denotational semantics of the extraction language needs to be developed), Artificial intelligence technologies (since the system will have an automatic theorem proving component).
1. To investigate the theoretical foundation of a logic for the automatic synthesis of provably correct computer programs.
2. To develop a prototype the implements program extraction along the lines of the first objective.
The student will prove general theorems showing the correctness of extracted programs and will use advanced programming techniques (monadic effects) to implement program extraction.
The project mainly resides in the areas of Theoretical Computer Science, Logic and combinatorics,
Verification and correctness, but it also intersects substantially with Mathematical analysis (since the main applications are in analysis), Natural language processing (since the system will contain a natural language interface), Programming languages and compilers (since the operational and denotational semantics of the extraction language needs to be developed), Artificial intelligence technologies (since the system will have an automatic theorem proving component).
Organisations
People |
ORCID iD |
| Ulrich Berger (Primary Supervisor) | |
| Olga Petrovska (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509553/1 | 01/10/2016 | 30/06/2022 | |||
| 1818640 | Studentship | EP/N509553/1 | 01/10/2016 | 31/07/2020 | Olga Petrovska |
| Description | - the underlying logical system improved and extended, which enabled a less restrictive approach to program extraction; - the soundness of the underlying theory proven; - the first prototype of the proof system released and used to successfully extract a number of executable programs. |
| Exploitation Route | - academic route: the existing logical system can be used as a base for further extension. Additional rules will improve the flexibility of the system. The theorems saved within the prototype proof assistant can be utilized to create more complex proofs. - non-academic route: the theory can be used to improve and extend the functionalities of the existing interactive theorem provers. |
| Sectors | Digital/Communication/Information Technologies (including Software),Transport,Other |
| Description | Talk - "Natural Language Proofs for Program Extraction" at PCC 2017 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | "The aim of PCC is to stimulate research in proof theory, computation, and complexity, focusing on issues which combine logical and computational aspects. Topics may include applications of formal inference systems in computer science, as well as new developments in proof theory motivated by computer science demands. Specific areas of interest are (non-exhaustively listed) foundations for specification and programming languages, logical methods in specification and program development including program extraction from proofs, type theory, new developments in structural proof theory, and implicit computational complexity." (PCC website) Abstract of the talk: Common software development techniques usually include substantial testing and bug fixing process. This process is costly in terms of time. It is prone to human errors as new bugs can be introduced and certain aspects may be overlooked due to testing not being exhaustive in many cases. An alternative approach to software development is program extraction. This technique implies proving correctness properties of software specifications formally in a proof assistant environment and then extracting software from such proof. However, most commonly used proof assistants are very restrictive in terms of language they use. The aim of this research is allowing a more natural proof style and avoiding the need to adjust to the proof assistant's requirements. Script is a prototype proof search system that is currently being developed as a part of this research. Its aim is creating a pipeline, which starts with natural language proofs as its input and enables to extract correct programs in the end of the process. In Script natural language proofs are transformed into their formal representations. Namely, each phrase in the proof script is processed by the system and is added to the context of the proof. Proof search checks whether it is possible to derive conclusions stated in the proof script using natural deduction rules. The formal system used is currently first-order logic, but the ultimate goal is to extend it to a constructive version of Church's simple theory of types, which is a formulation of higher-order logic based on simply typed lambda calculus. When the user enters a complete natural proof, the system should generate a formal proof object in natural deduction and extract a program using a realizability interpretation. Realizability gives a theoretical basis for program extraction. In this particular case lambda terms are used as realizers. Since lambda calculus can represent notions and properties of all functional languages, transforming lambda terms into actual program is fairly simple. The system has a lot in common with the interactive proof system Minlog developed at the University of Munich. The main difference is that our realizers are type free while Minog uses typed realizers. The aim of this talk is to present theoretical background of program extraction from proofs, and realizability interpretation in particular as proposed by U.Berger/T.Hou. It will also provide a brief overview of language used in current proof assistants and give an outline of the main challenges of processing natural language proofs in a proof assistant environment. Additionally, we will report on the initial work, namely current development stage of Script. The talked inspired a lively discussion, which provided some valuable ideas as to how this research can be extended. |
| Year(s) Of Engagement Activity | 2017 |
| URL | https://www.irit.fr/PCC2017/ |
| Description | Talk: "Intuitionistic Fixed Point Logic and Program Extraction (with Prawf)" at BCTCS 2020 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Postgraduate students |
| Results and Impact | "The British Colloquium for Theoretical Computer Science (BCTCS) is an annual event for UK-based researchers in theoretical computer science. A central aspect of BCTCS is the training of PhD students, providing an environment for students to gain experience in presenting their work, to broaden their outlook on the subject, and to benefit from contact with established researchers. The scope of the colloquium includes all aspects of theoretical computer science, including automata theory, algorithms, complexity theory, semantics, formal methods, concurrency, types, languages and logics." (BCTCS 2020 website) During the colloquium I presented our proof assistant, which works with Intuitionistic Fixed Point Logic. I gave a demo of an addition program extracted from a logical proof. The audience was interested and the talk provoked a discussion on how the logic as well as the functionalities of the tool can be extended futher. |
| Year(s) Of Engagement Activity | 2020 |
| URL | https://cs.swansea.ac.uk/bctcs2020/abstracts |
| Description | Talk: "Intuitionistic Fixed Point Logic and Program Extraction" at CCC 2018 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | "CCC is a workshop series bringing together researchers from exact real number computation, computable analysis, effective descriptive set theory, constructive analysis, and related areas. The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correct algorithms for computations with real numbers and related analytical data, which are of increasing importance in safety critical applications and scientific computation." (CCC website) CCC gathers together specialists that are specifically interested in computations involving infinite data. The partcipants were very interested in Intuitionistic Fixed Point Logic (IFP) and the opportunities that it provides when used as an underlying logical system for program extraction. Interesting and useful discussions regarding the use of IFP sn its extension Concurrent IFP (CIFP) took place not only after the talk but also during the whole duration of the conference/ |
| Year(s) Of Engagement Activity | 2018 |
| URL | http://cid.uni-trier.de/conferences/ccc-2018/ |
| Description | Talk: "Optimized Program Extraction for Induction and Coinduction" at CiE 2018 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | "CiE 2018 is the fourteenth conference organized by CiE (Computability in Europe), a European association of mathematicians, logicians, computer scientists, philosophers, physicists and others interested in new developments in computability and their underlying significance for the real world." (CiE 2018 website) During this conference I presented Intuitionistic Fixed Point Logic. The motivation behind such logic is creation of suitable formal systems for exploiting Curry-Howard correspondence to extract useful programs from proofs about abstract mathematics. The talk sparked questions and discussion afterwards. |
| Year(s) Of Engagement Activity | 2018 |
| URL | https://cie2018.uni-kiel.de/accepted-papers/ |
| Description | Talk: "Prawf: An Interactive Proof Assistant for Program Extraction" at CiE 2020 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | "The CiE conferences serve as an interdisciplinary forum for research in all aspects of computability, foundations of computer science, logic, and theoretical computer science, as well as the interplay of these areas with practical issues in computer science and with other disciplines such as biology, mathematics, philosophy, or physics." (CiE 2020 website) During this conference I presented our proof assistant based on Intuitionistic Fixed Point Logic. The audience included computer scientists and mathematicians from all over Europe, both postgraduate students and estabilished researches. They were very interested in the demo, which showcased an example of extracting executable programs from proofs. |
| Year(s) Of Engagement Activity | 2020 |
| URL | https://cie2020.wordpress.com/accepted-papers-2/ |