Abstract
Over the last few decades, software has become essential for the
proper functioning of systems in the modern world. Formal verication
techniques are slowly being adopted in various industrial application areas,
and there is a big demand for research in the theory and practice of
formal techniques to achieve a wider acceptance of tools for verication.
We present three projects concerned with applications of certied
programming techniques and proof assistants in the area of programming
language theory and mathematics.
The rst project is about a certied compilation technique for a
domain-specic programming language for nancial contracts (the CL
language). The code in CL is translated into a simple expression language
well-suited for integration with software components implementing
Monte Carlo simulation techniques (pricing engines). The compilation
procedure is accompanied with formal proofs of correctness carried out in
the Coq proof assistant. Moreover, we develop techniques for capturing
the dynamic behavior of contracts with the passage of time. These techniques
potentially allow for ecient integration of contract specications
with high-performance pricing engines running on GPGPU hardware.
The second project presents a number of techniques that allow for
formal reasoning with nested and mutually inductive structures built up
from nite maps and sets (also called semantic objects), and at the same
time allow for working with binding structures over sets of variables.
The techniques, which build on the theory of nominal sets combined
with the ability to work with multiple isomorphic representations of -
nite maps, make it possible to give a formal treatment, in Coq, of a
higher-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 modules
and provides the foundation for a higher-order module language for
Futhark, an optimising compiler targeting data-parallel architectures,
such as GPGPUs.
The third project is related to homotopy type theory (HoTT), a new
branch of mathematics based on a fascinating idea connecting type theory
and homotopy theory. HoTT provides us with a new foundation for
mathematics allowing for developing machine-checkable proofs in various
areas of computer science and mathematics. Along with Vladimir
Voevodsky's univalence axiom, HoTT oers a formal treatment of the
informal mathematical principle: equivalent structures can be identied.
However, in some cases, the notion of weak equality available in HoTT
leads to the innite coherence problem when dening internally certain
structures (such as a type of n-restricted semi-simplicial types, inverse
diagrams and so on). We explain the basic idea of two-level type theory, a
version of Martin-Löf type theory with two equality types: the rst acts
as the usual equality of homotopy type theory, while the second allows us
to reason about strict equality. In this system, we can formalise results of
partially meta-theoretic nature. We develop and explore in details how
two-level type theory can be implemented in a proof assistant, providing
a prototype implementation in the proof assistant Lean. We demonstrate
an application of two-level type theory by developing some results from
the theory of inverse diagrams using our Lean implementation.
proper functioning of systems in the modern world. Formal verication
techniques are slowly being adopted in various industrial application areas,
and there is a big demand for research in the theory and practice of
formal techniques to achieve a wider acceptance of tools for verication.
We present three projects concerned with applications of certied
programming techniques and proof assistants in the area of programming
language theory and mathematics.
The rst project is about a certied compilation technique for a
domain-specic programming language for nancial contracts (the CL
language). The code in CL is translated into a simple expression language
well-suited for integration with software components implementing
Monte Carlo simulation techniques (pricing engines). The compilation
procedure is accompanied with formal proofs of correctness carried out in
the Coq proof assistant. Moreover, we develop techniques for capturing
the dynamic behavior of contracts with the passage of time. These techniques
potentially allow for ecient integration of contract specications
with high-performance pricing engines running on GPGPU hardware.
The second project presents a number of techniques that allow for
formal reasoning with nested and mutually inductive structures built up
from nite maps and sets (also called semantic objects), and at the same
time allow for working with binding structures over sets of variables.
The techniques, which build on the theory of nominal sets combined
with the ability to work with multiple isomorphic representations of -
nite maps, make it possible to give a formal treatment, in Coq, of a
higher-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 modules
and provides the foundation for a higher-order module language for
Futhark, an optimising compiler targeting data-parallel architectures,
such as GPGPUs.
The third project is related to homotopy type theory (HoTT), a new
branch of mathematics based on a fascinating idea connecting type theory
and homotopy theory. HoTT provides us with a new foundation for
mathematics allowing for developing machine-checkable proofs in various
areas of computer science and mathematics. Along with Vladimir
Voevodsky's univalence axiom, HoTT oers a formal treatment of the
informal mathematical principle: equivalent structures can be identied.
However, in some cases, the notion of weak equality available in HoTT
leads to the innite coherence problem when dening internally certain
structures (such as a type of n-restricted semi-simplicial types, inverse
diagrams and so on). We explain the basic idea of two-level type theory, a
version of Martin-Löf type theory with two equality types: the rst acts
as the usual equality of homotopy type theory, while the second allows us
to reason about strict equality. In this system, we can formalise results of
partially meta-theoretic nature. We develop and explore in details how
two-level type theory can be implemented in a proof assistant, providing
a prototype implementation in the proof assistant Lean. We demonstrate
an application of two-level type theory by developing some results from
the theory of inverse diagrams using our Lean implementation.
| Originalsprog | Engelsk |
|---|
| Forlag | Department of Computer Science, Faculty of Science, University of Copenhagen |
|---|---|
| Status | Udgivet - 2017 |