Certified Programming with Dependent Types
Abstract
The project has substantially contributed to the development of Type Theory as an effective tool to formalize complex mathematical arguments in a concise and natural way and use this technology for the verification of software and hardware systems. It also delivers a novel way to underpin mathematical constructions by using structural reasoning instead of set-theoretic reasoning which is less modular and depends heavily on the choice of representations.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 14, 2021
- Accession Number
- AD1154805
Entities
People
- Thorsten Altenkirch
Organizations
- University of Nottingham