A System of Dependent Types, with an Implementation and a Philosophy
Logic
2016-10-31 v2
Abstract
This is my working paper on a proposed logical framework for the practice of mathematics, which is paralleled by philosophical considerations and a computer implementation (a variant of Automath). Updated 10/27/2016 with a version from 10/22/2016. New versions are regularly posted on the author's web page at http://math.boisestate.edu/%7Eholmes/automath/ which is a directory containing various related files.
Keywords
Cite
@article{arxiv.1607.01817,
title = {A System of Dependent Types, with an Implementation and a Philosophy},
author = {M. Randall Holmes},
journal= {arXiv preprint arXiv:1607.01817},
year = {2016}
}
Comments
bibliography has been added