A System of Dependent Types, with an Implementation and a Philosophy
M. Randall Holmes
TL;DR
This paper presents a logical framework for mathematics based on dependent types, including a philosophical perspective and a computer implementation, aiming to enhance formalization and understanding of mathematical practice.
Contribution
It introduces a novel dependent type system framework with an associated implementation and philosophical discussion, advancing formal methods in mathematics.
Findings
Development of a dependent type-based logical framework
Implementation of a variant of Automath
Philosophical insights into mathematical formalization
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Computability, Logic, AI Algorithms