Agent-Based Logics in Dependent Type Theory
This thesis is on the formalisation of mathematics in Martin-Löf type theory. This is a class of dependently-typed functional programming languages whose rules form a language suitable for the statement and proof of mathematical theorems. Programs in type theory can be mechanically checked to be wel...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/81134/ |