From 012981244762a269e81cadea0b27e87d6497590b Mon Sep 17 00:00:00 2001 From: Ailrun Date: Sat, 9 Nov 2024 16:50:53 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20Beluga-l?= =?UTF-8?q?ang/McTT@9566894d5c6e6346811f8785e2494f093f00896b=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- index.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/index.html b/index.html index 1990413..11a104b 100644 --- a/index.html +++ b/index.html @@ -55,8 +55,8 @@

McTT: A -Bottom-up Approach to Implementing A Proof Assistant

+id="mctt-building-a-correct-by-construction-proof-checkers-for-type-theories">McTT: +Building A Correct-By-Construction Proof Checkers For Type Theories

McTT is a verified, runnable typechecker for Martin-Löf type theory. This project provides an executable, to which we can feed a program in Martin-Löf type theory to check whether this program has the specified