TY - BOOK

T1 - Adventures in Formalisation

T2 - Financial Contracts, Modules, and Two-Level Type Theory

AU - Annenkov, Danil

PY - 2017

Y1 - 2017

N2 - Over the last few decades, software has become essential for theproper functioning of systems in the modern world. Formal vericationtechniques are slowly being adopted in various industrial application areas,and there is a big demand for research in the theory and practice offormal techniques to achieve a wider acceptance of tools for verication.We present three projects concerned with applications of certiedprogramming techniques and proof assistants in the area of programminglanguage theory and mathematics.The rst project is about a certied compilation technique for adomain-specic programming language for nancial contracts (the CLlanguage). The code in CL is translated into a simple expression languagewell-suited for integration with software components implementingMonte Carlo simulation techniques (pricing engines). The compilationprocedure is accompanied with formal proofs of correctness carried out inthe Coq proof assistant. Moreover, we develop techniques for capturingthe dynamic behavior of contracts with the passage of time. These techniquespotentially allow for ecient integration of contract specicationswith high-performance pricing engines running on GPGPU hardware.The second project presents a number of techniques that allow forformal reasoning with nested and mutually inductive structures built upfrom nite maps and sets (also called semantic objects), and at the sametime allow for working with binding structures over sets of variables.The techniques, which build on the theory of nominal sets combinedwith the ability to work with multiple isomorphic representations of -nite maps, make it possible to give a formal treatment, in Coq, of ahigher-order module system, including the ability to eliminate entirely,at compile time, abstraction barriers introduced by the module system.The development is based on earlier work on static interpretation of modulesand provides the foundation for a higher-order module language forFuthark, an optimising compiler targeting data-parallel architectures,such as GPGPUs.The third project is related to homotopy type theory (HoTT), a newbranch of mathematics based on a fascinating idea connecting type theoryand homotopy theory. HoTT provides us with a new foundation formathematics allowing for developing machine-checkable proofs in variousareas of computer science and mathematics. Along with VladimirVoevodsky's univalence axiom, HoTT oers a formal treatment of theinformal mathematical principle: equivalent structures can be identied.However, in some cases, the notion of weak equality available in HoTTleads to the innite coherence problem when dening internally certainstructures (such as a type of n-restricted semi-simplicial types, inversediagrams and so on). We explain the basic idea of two-level type theory, aversion of Martin-Löf type theory with two equality types: the rst actsas the usual equality of homotopy type theory, while the second allows usto reason about strict equality. In this system, we can formalise results ofpartially meta-theoretic nature. We develop and explore in details howtwo-level type theory can be implemented in a proof assistant, providinga prototype implementation in the proof assistant Lean. We demonstratean application of two-level type theory by developing some results fromthe theory of inverse diagrams using our Lean implementation.

AB - Over the last few decades, software has become essential for theproper functioning of systems in the modern world. Formal vericationtechniques are slowly being adopted in various industrial application areas,and there is a big demand for research in the theory and practice offormal techniques to achieve a wider acceptance of tools for verication.We present three projects concerned with applications of certiedprogramming techniques and proof assistants in the area of programminglanguage theory and mathematics.The rst project is about a certied compilation technique for adomain-specic programming language for nancial contracts (the CLlanguage). The code in CL is translated into a simple expression languagewell-suited for integration with software components implementingMonte Carlo simulation techniques (pricing engines). The compilationprocedure is accompanied with formal proofs of correctness carried out inthe Coq proof assistant. Moreover, we develop techniques for capturingthe dynamic behavior of contracts with the passage of time. These techniquespotentially allow for ecient integration of contract specicationswith high-performance pricing engines running on GPGPU hardware.The second project presents a number of techniques that allow forformal reasoning with nested and mutually inductive structures built upfrom nite maps and sets (also called semantic objects), and at the sametime allow for working with binding structures over sets of variables.The techniques, which build on the theory of nominal sets combinedwith the ability to work with multiple isomorphic representations of -nite maps, make it possible to give a formal treatment, in Coq, of ahigher-order module system, including the ability to eliminate entirely,at compile time, abstraction barriers introduced by the module system.The development is based on earlier work on static interpretation of modulesand provides the foundation for a higher-order module language forFuthark, an optimising compiler targeting data-parallel architectures,such as GPGPUs.The third project is related to homotopy type theory (HoTT), a newbranch of mathematics based on a fascinating idea connecting type theoryand homotopy theory. HoTT provides us with a new foundation formathematics allowing for developing machine-checkable proofs in variousareas of computer science and mathematics. Along with VladimirVoevodsky's univalence axiom, HoTT oers a formal treatment of theinformal mathematical principle: equivalent structures can be identied.However, in some cases, the notion of weak equality available in HoTTleads to the innite coherence problem when dening internally certainstructures (such as a type of n-restricted semi-simplicial types, inversediagrams and so on). We explain the basic idea of two-level type theory, aversion of Martin-Löf type theory with two equality types: the rst actsas the usual equality of homotopy type theory, while the second allows usto reason about strict equality. In this system, we can formalise results ofpartially meta-theoretic nature. We develop and explore in details howtwo-level type theory can be implemented in a proof assistant, providinga prototype implementation in the proof assistant Lean. We demonstratean application of two-level type theory by developing some results fromthe theory of inverse diagrams using our Lean implementation.

UR - https://soeg.kb.dk/permalink/45KBDK_KGL/fbp0ps/alma99122733093305763

M3 - Ph.D. thesis

BT - Adventures in Formalisation

PB - Department of Computer Science, Faculty of Science, University of Copenhagen

ER -