A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
lib
scripts
src
.gitignore
.gitmodules
.travis.yml
README.md
dependent_lcf.cm
dependent_lcf.mlb
development.cm
example.sml
lcf_abt.cm
lcf_abt.mlb
sml.json

README.md

This repository contains a library for building tactic-based refiners in the LCF and Nuprl tradition.

Dependent LCF: modernized refinement proof

Dependent LCF is a modernization of the old LCF tactic system, to deal with dependent refinement properly. A proof state is a telescope of judgments, where each judgment binds a metavariable in the rest of the telescope, together with a term that takes its free metavariables from the telescope.

The telescope corresponds to the list of subgoals in LCF, and the open term corresponds to the "validation" in LCF. Whereas in Classic LCF, the validation was a computational function from evidence to evidence, here it is a piece of evidence with free variables; this design choice is forced by the categorical semantics for Dependent LCF, and suggests that the computational character of validations in Classic LCF is a design which does not generalize cleanly.

Instructions

git submodule update --init --recursive
rlwrap sml
> CM.make "development.cm";