Why Higher-Order Logic Is a Good Formalisation for Hardware
Postedabout 2 months ago
cl.cam.ac.ukTechstory
calmneutral
Debate
0/100
Formal VerificationHardware DesignHigher-Order Logic
Key topics
Formal Verification
Hardware Design
Higher-Order Logic
A 1985 technical report discusses the use of higher-order logic for specifying and verifying hardware, with a single comment providing a brief summary of the report's abstract.
Snapshot generated from the HN discussion
Discussion Activity
Light discussionFirst comment
N/A
Peak period
1
Start
Avg / period
1
Key moments
- 01Story posted
Nov 5, 2025 at 8:37 AM EST
about 2 months ago
Step 01 - 02First comment
Nov 5, 2025 at 8:37 AM EST
0s after posting
Step 02 - 03Peak activity
1 comments in Start
Hottest window of the conversation
Step 03 - 04Latest activity
Nov 5, 2025 at 8:37 AM EST
about 2 months ago
Step 04
Generating AI Summary...
Analyzing up to 500 comments to identify key contributors and discussion patterns
ID: 45822688Type: storyLast synced: 11/17/2025, 7:53:27 AM
Want the full context?
Jump to the original sources
Read the primary article or dive into the live Hacker News thread when you're ready.
Why higher-order logic is a good formalisation for specifying and verifying hardware
Mike Gordon
September 1985, 28 pages
DOI https://doi.org/10.48456/tr-77
Abstract
Higher order logic was originally developed as a foundation for mathematics. In this paper we show how it can be used as: 1. a hardware description language, and 2. a formalism for proving that designs meet their specifications.
Examples are given which illustrate various specification and verification techniques. These include a CMOS inverter, a CMOS full adder, an n-bit ripple-carry adder, a sequential multiplier and an edge-triggered D-type register.
See also https://lawrencecpaulson.github.io/2023/01/04/Hardware_Verif... and "Interactive Formal Verification, Lecture 11: Hardware Verification" by Lawrence Paulson https://www.youtube.com/watch?v=KVdgoEpo4uI&list=PLVdBoNna-4...