Skip to content

Commit

Permalink
Deploying to gh-pages from @ 8835b73 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
Ailrun committed Nov 8, 2024
1 parent 87e6fab commit fd5f885
Showing 1 changed file with 9 additions and 8 deletions.
17 changes: 9 additions & 8 deletions index.html
Original file line number Diff line number Diff line change
Expand Up @@ -55,23 +55,24 @@
</head>
<body>
<h1
id="mcltt-a-bottom-up-approach-to-implementing-a-proof-assistant">McLTT:
A Bottom-up Approach to Implementing A Proof Assistant</h1>
<p>McLTT is a verified, runnable typechecker for Martin-Löf type theory.
id="mctt-a-bottom-up-approach-to-implementing-a-proof-assistant">McTT: A
Bottom-up Approach to Implementing A Proof Assistant</h1>
<p>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
type. McLTT is novel in that it is implemented and verified in Coq. More
type. McTT is novel in that it is implemented and verified in Coq. More
specifically, we proved that the typechecking algorithm extracted from
Coq is sound and complete: a program passes typechecker if and only if
it is a well-typed program in MLTT. This is the first verified proof
assistant (despite being elementary) and serves as a basis for future
extensions.</p>
<h2 id="online-documentation">Online Documentation</h2>
<p>We have generated a <a href="dep.html">Coqdoc</a> for browsing our
Coq proof.</p>
<p>We have generated a <a
href="https://beluga-lang.github.io/McTT/dep.html">Coqdoc</a> for
browsing our Coq proof.</p>
<h2 id="architecture">Architecture</h2>
<p>McLTT has the following architecture:</p>
<pre><code> | source code of McLTT
<p>McTT has the following architecture:</p>
<pre><code> | source code of McTT
v
+-------+
| lexer | OCaml code generated by ocamllex
Expand Down

0 comments on commit fd5f885

Please sign in to comment.