Certified Programming with Dependent Types

reportActive / Technical Report | Accesssion Number: AD1154805 | Open PDF

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.

Author(s):
Altenkirch, Thorsten
Author Organization(s):
UNIVERSITY OF NOTTINGHAM UNIVERSITY PK
Funding Organization(s):
AFOSR, ARLINGTON , VA
Document Type:
Technical Report/Final Report
Publication Date:
2021 Sep 14
Pagination:
11

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution Code:
A - Approved For Public Release
Distribution Statement: Public Release

RECORD

Collection: TRECMS
Identifying Numbers
Report Number(s):
AFRL-AFOSR-VA-TR-2022-0053
Grant Number(s):
FA9550-16-1-0029
Program Element Number(s):
PE61102F
Subject Terms
Communities of Interest:
No COI(s) Identified
Descriptor(s):
scientific research, language, computations, computer science, buildings and structures, computers, construction, mathematics, christianity, computer programming, containers, department of defense, information operations, reasoning, symposia, workshops, schools
Subject Categories:
Mathematical and Computer Sciences
Creation Date:
2021 Dec 09
Update Date:
2022 Jan 20