Spelling suggestions: "subject:"agua"" "subject:"aga""
1 |
A Formal Proof of Feit-Higman Theorem in AgdaRao, Balaji R January 2014 (has links) (PDF)
In this thesis we present a formalization of the combinatorial part of the proof of Feit-Higman theorem on generalized polygons. Generalised polygons are abstract geometric structures that generalize ordinary polygons and projective planes. They are closely related to finite groups.
The formalization is carried out in Agda, a dependently typed functional programming language and proof assistant based on the intuitionist type theory by Per Martin-Löf.
|
2 |
Univalent Types, Sets and Multisets : Investigations in dependent type theoryRobbestad Gylterud, Håkon January 2017 (has links)
This thesis consists of four papers on type theory and a formalisation of certain results from the two first papers in the Agda language. We cover topics such as models of multisets and sets in Homotopy Type Theory, and explore ideas of using type theory as a language for databases and different ways of expressing dependencies between terms. The two first papers build on work by Aczel 1978. We establish that the underlying type of Aczel’s model of set theory in type theory can be seen as a type of multisets from the perspective of Homotopy Type Theory, and we identify a suitable subtype which becomes a model of set theory in which equality of sets is the identity type. The third paper is joint work with Henrik Forssell and David I .Spivak and explores a certain model of type theory, consisting of simplicial complexes, from the perspective of database theory. In the fourth and final paper, we consider two approaches to unraveling the dependency structures between terms in dependent type theory, and formulate a few conjectures about how these two approaches relate.
|
3 |
Do-it-Yourself Module Systems / Extending Dependently-Typed Languages to Implement Module System Features In The Core LanguageAl-hassy, Musa January 2021 (has links)
In programming languages, record types give a universe of discourse (via so-called Σ-types);
parameterised record types fix parts of that universe ahead of time (via Π-types), and algebraic
datatypes give us first-class syntax (via W-types), which can then be used to program, e.g.,
evaluators and optimisers. A frequently-encountered issue in library design for statically-typed
languages is that, for example, the algebraic datatype implementing the first-class view of the
language induced by a record declaration cannot be defined by simple reference to the record
type declaration, nor to any common “source”. This leads to unwelcome repetition, and to
maintenance burdens. Similarly, the “unbundling problem” concerns similar repetition that
arises for variants of record types where some fields are turned into parameters.
The goal of this thesis is to show how, in dependently-typed languages (DTLs), algebraic
datatypes and parameterised record types can be obtained from a single pragmatic declaration
within the dependently-typed language itself, without using a separate “module language”. Besides this practical shared declaration interface, which is extensible in the language, we also find
that common data structures correspond to simple theories.
Put simply, the thesis is about making tedious and inexpressible patterns of programming
in DTLs (dependently typed languages) become mechanical and expressible. The situations
described above occur frequently when working in a dependently-typed language, and it is
reasonable enough to have the computer handle them.
We develop a notion of contexts that serve as common source for definitions of algebraic
datatype and of parameterised record types, and demonstrate a “language” of “package operations” that enables us to avoid the above-mentioned replication that pervades current library
developments.
On the one hand, we demonstrate an implementation of that language as integrated editor functionality — this makes it possible to directly emulate the different solutions that are
employed in current library developments, and refactor these into a shape that uses single declaration of contexts, thus avoiding the usual repetition that is otherwise required for provision
of record types at different levels of parameterisation and of algebraic datatypes.
On the other hand, we will demonstrate that the power of dependently-typed languages
is sufficient to implement such package operations in a statically-typed manner within the
language; using this approach will require adapting to the accordingly-changed library interfaces.
Although our development uses the dependently-typed programming language Agda throughout, we emphasise that the idea is sufficiently generic to be implemented in other DTLs. / Thesis / Doctor of Philosophy (PhD) / There are things we want to use from various perspectives, our tools show that this is possible without any duplication and in a practical and efficient fashion.
|
Page generated in 0.043 seconds