Skip to main content
19 votes

What is known about the consistency of proof assistant metatheories?

This is more of a comment than an answer. I really look forward to the answers, but it should be noted that there are a lot of subtleties when saying that a system is consistent. First, a logical ...
Jason Rute's user avatar
  • 8,685
11 votes

What is known about the consistency of proof assistant metatheories?

I am not familiar enough with the literature on this question to be able to point to specific papers, but allow me to make a basic sketch on how one can set up set-theoretic models of type theories. I ...
Andrej Bauer's user avatar
  • 9,194
11 votes
Accepted

What is realignment and is it useful in non-univalent theories?

This is a very good question. What is realignment for? One application of realignment that is particularly useful is to construct a cumulative hierarchy of universes; what cumulativity means in the &...
Jonathan Sterling's user avatar
6 votes

What is known about the consistency of proof assistant metatheories?

Because HOL is so weak, it has had a quite a bit of work done on its semantics and soundness, both at the logic level, and in terms of implementations. The bibliography in Oskar Abrahamsson’s recent ...
Michael Norrish's user avatar
5 votes
Accepted

State of art for observational equality, on the injectivity requirement

Is the injectivity of π‘‡π‘‡π‘œπ‘π‘ /πΆπΆπ‘œπ‘π‘  also anti-classical? It isn't. The setoid model in the TTobs paper supports LEM (meaning that every setoid is empty or nonempty). This note explains that ...
András Kovács's user avatar
5 votes

Programming language metatheory in Lean 4?

We've been developing the metatheory of SSA based programs at https://github.com/opencompl/ssa/. In particular, we develop: An intrinsically well-typed encoding of SSA+Regions A mechanized peephole ...
Siddharth Bhat's user avatar
3 votes

Programming language metatheory in Lean 4?

Eventually we went ahead and did a bunch of metatheory in Lean 4 anyhow. My work with my PhD student Jad Ghalayini on explicit refinement types (at ICFP 2023) was formalised in Lean 4 here. The ...
Neel Krishnaswami's user avatar
2 votes

Programming language metatheory in Lean 4?

An exciting direction is the metatheory of Lean 4 itself. In Sebastian Ullrich's dissertation An Extensible Theorem Proving Frontend, he formalizes the semantics of Lean 4's do notation in Lean 4 ...
Jason Rute's user avatar
  • 8,685

Only top scored, non community-wiki answers of a minimum length are eligible