HackerPapers

arXiv:1905.05970cs.LO

HolPy: Interactive Theorem Proving in Python

Bohua Zhan

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

HolPy is an interactive theorem proving system implemented in Python. It uses higher-order logic as the logical foundation. Its main features include a pervasive use of macros in producing, checking, and storing proofs, a JSON-based format for theories, and an API for implementing proof automation and other extensions in Python. A point-and-click-based user interface is implemented for general-purpose theorem proving. We describe the main design decisions of HolPy, current applications, and plans for the future.

arXiv comments
8 pages
Journal reference
DOI
Subjects
cs.LOLogic in Computer Science

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Jan 2020 to Jan 2020. Found in 1 HN submission from May 2019 to May 2019. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Show HN: CrossHair – SMT Assisted Testing for Python 1 comment

    • Very cool! Ever looked at the Viper project? It's the only other system in python that I know of targeting pre and post conditions https://www.pm.inf.ethz.ch/research/viper.html https://www.pm.inf.ethz.ch/research/nagini.html Another thing that might be of interest is HOLpy. I…

      philzookView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.