vix.ing · top · new · best · stats · spec

A System of Dependent Types, with an Implementation and a Philosophy

2016/07/06 by M. Randall Holmes, Holmes, M. Randall
Computer Science · Mathematics · #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #math.LO

paper · pdf · doi:10.48550/arxiv.1607.01817

bibliography has been added

openalex publication_date 2016/07/06 · arxiv created 2016/10/27 · arxiv updated 2016/10/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related