CoqHM: A Formally Verified Hindley-Milner Type Inference System

This project is a formal implementation and verification of the Hindley-Milner type inference algorithm using the Coq proof assistant. The goal is to build a type inference engine for a small functional language and to prove, with mathematical certainty, that the algorithm is sound.

Getting Started

Prerequisites

• Rocq (version 9.0.0 or later recommended)
• Make

Installation & Build

1. Clone the repository:

   git clone https://github.com/BIRSAx2/CoqHM.git
   cd CoqHM

2. Build the project: Compile all Coq files and run tests with a single command.

   make

   To clean the build artifacts, run:

   make clean

Contributing

Commit Convention

This project uses Conventional Commits for automated versioning and changelog generation. Please follow this format for all commits.

Commit Message Format

<type>[optional scope]: <description>

[optional body]

[optional footer(s)]

Commit Types

• feat: A new feature (triggers a minor version bump)
• fix: A bug fix in the logic or proofs (triggers a patch version bump)
• docs: Documentation only changes
• style: Changes that do not affect the meaning of the code (formatting, etc.)
• refactor: A code change that neither fixes a bug nor adds a feature
• test: Adding missing tests or correcting existing tests
• chore: Changes to the build process, CI, or other auxiliary tools
• proof: A commit focused exclusively on proving existing lemmas or theorems.

Breaking Changes

To indicate a breaking change that requires a major version bump, add ! after the type/scope or include BREAKING CHANGE: in the footer.

# Example of a breaking change
git commit -m "refactor!: rename core 'infer' function to 'type_infer'

BREAKING CHANGE: The main inference entrypoint has been renamed. This will require updates in all downstream test files."

Project Structure

• .github/workflows/: Contains CI/CD automation pipelines.
• src/: The core compiler logic and proofs.
• tests/: Unit and integration tests for the Coq modules.
• _CoqProject: Coq project configuration file.

CI/CD Pipeline

This project is equipped with a professional CI/CD pipeline that automates:

• Linting: Commit messages on Pull Requests are automatically linted.
• Building & Testing: Every push and PR is automatically built and tested.
• Automated Releases: Merges to main automatically generate version numbers, tags, and release notes based on the commit messages.