DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
AD1085817
Title:
The UniMath Library for Type Theory and Programming Languages
Report Date:
2019-04-14
Abstract:
Matthew Weaver, Ph.D. student at Princeton University, worked under the direction of Lennart Beringer and also (initially) under Voevodsky, and also in collaboration with Dan Licata (Wesleyan University) and Dimitris Tsementzis (Rutgers). Weaver began to develop bicubical directed type theory in collaboration with Daniel R. Licata. Bicubical directed type theory is a constructive model of type theory in where types are augmented with higher-dimensional structure in two ways: beyond being just a set of terms, each type also has terms corresponding to paths between terms in the type, and terms representing directed morphisms from one term to another. This additional higher-dimensional data is organized 'cubically' to improve the computational properties of the theory. Given types contain two notions of paths the undirected paths and directed morphismsevery term is represented as two cubes: the first containing the path structure it represents and the other the morphism structure. The goal of bicubical directed type theory is for it to ultimately be a constructive model of a type theory with directed univalence. Lennart Beringer, research scholar in the Computer Science Department at Princeton University, carried out research on dependently-typed verification of security protocols in Coq. This work used the Verified Software Toolchain (VST), an implementation of impredicative higher-order concurrent separation logic for the C language. VST's step-indexed semantic model Appel et al., 2014, foundationally justifies functional correctness assertions with respect to the operational semantics of Clight, the topmost intermediate language of the CompCert verified C compiler. Benedikt Ahrens, Birmingham Fellow at University of Birmingham, UK, carried out research into the use of categorical structures for the semantics of homotopy type theory. Two papers were published, one was accepted, one was submitted, and another is in progress.
Document Type:
Conference:
Journal:
Pages:
14
File Size:
1.16MB
FA9550-17-1-0363
(FA95501710363);
Contracts:
Grants:
Distribution Statement:
Approved For Public Release
