Skip to main content
22 votes
Accepted

When should I use De Bruijn levels instead of indices?

If we want to do evaluation in the presence of free variables ("open" evaluation), then De Bruijn levels are essential, precisely because of their support for cost-free weakening. Generally, ...
András Kovács's user avatar
17 votes
Accepted

Constructive proof of strong normalization for simply typed lambda calculus

As Dan Doel says in the comments, the reason Kőnig's lemma is used is that Girard's definition of strong normalization is constructively too weak. It's defined as the non-existence of infinite ...
András Kovács's user avatar
15 votes
Accepted

Is there something special about weak head normal form used with proof assistants?

The application rule in a dependent type system looks a bit like this: $$\newcommand{\judge}[3]{{#1} \vdash {#2} : {#3}} \newcommand{\jeq}[3]{{#1} \vdash {#2} \equiv {#3}} \frac{\displaystyle \judge{\...
Neel Krishnaswami's user avatar
7 votes

Constructive proof of strong normalization for simply typed lambda calculus

For a modern take on the proof, you can have a look at POPLmark Reloaded. The paper's appendix explains in great details what the (sometimes technical) proofs are. The paper comes with various ...
gallais's user avatar
  • 1,256
7 votes

Comparison between proof assistants for coinductive structures and proofs

Here's my quick and dirty overview. I don't know Lean, so anyone who does is free to edit the answer to add it, but my impression is that co-induction isn't natively supported there yet. Coq: ...
Joey Eremondi's user avatar
6 votes

Is there something special about weak head normal form used with proof assistants?

Despite their quite technical appearance, weak head normal form also have a philosophical genesis. In Martin-Löf's meaning explanations, the canonical form of a term (its meaning) is defined by ...
Maximilian Doré's user avatar
5 votes
Accepted

LEM, the halting problem, the curry-howard correspondence -> deep connection?

Is it correct that the omission of LEM is the distinguishing characteristic of constructive logic as opposed to classical? Yes. Is it correct that the Curry-Howard correspondence is conditioned on ...
Mario Carneiro's user avatar
4 votes

Generic proof assistants/modularity of the proof assistants?

It sounds like you're after a logical framework, i.e., a system which allows you to reason within a given foundations. Isabelle is a bit more than this, it's a so-called "meta-logical framework&...
Alex Nelson's user avatar
  • 1,574
3 votes

Comparison between proof assistants for coinductive structures and proofs

I do not know much about other proof assistants, but as for Coq I can say that there are quite some resources around that you might benefit from. Here is a starting point. However, the current ...
Meven Lennon-Bertrand's user avatar
3 votes
Accepted

How to encode and manipulate (parallel) substitutions?

I can offer some exprerience with formalizing the syntax of type theory, see this Agda formalization. One important insight is that we should implement renamings first. These are like substitutions, ...
Andrej Bauer's user avatar
  • 9,593
3 votes

Is there any formalization (with any theorem prover) of the Bohm theorem for lambda-calculus?

Not sure whether this answers your request, but Łukasz Czajka has formalized in Coq his proof of confluence (and normalization) of the infinitary λ-calculus modulo (strongly) meaningless terms. In the ...
sparusaurata's user avatar
3 votes

untyped lambda expressions may not have normal forms; are they used (or OK to use) in proof assistants?

Firstly, for general recursion in the lambda calculus you need the Y-combinator: $$Y = \lambda f.(\lambda x.f (x\ x)) (\lambda x.f (x\ x))$$ which satisfies $Y\ g = g\ (Y\ g)$. But in general you can'...
Couchy's user avatar
  • 2,271
3 votes
Accepted

How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?

(This answer assumes you already know some of the basics of Lean as in Theorem Proving in Lean 4.) In a typical first logic class or set theory class in college, first order logic is presented as ...
Jason Rute's user avatar
  • 8,960
3 votes

LEM, the halting problem, the curry-howard correspondence -> deep connection?

Complexity theory in general has very low logical complexity. Almost all of it can be expressed in Peano arithmetic, and often in much weaker fragments of arithmetic. Furthermore, the most interesting ...
Andrej Bauer's user avatar
  • 9,593
2 votes
Accepted

What is the $\mu$ in the labmda calculus defined here?

What is the $\mu$ in above definition of lambda calculus (what is the associated formal system)? This system is (a variation of) the language PCF. This language has been a landmark in the study of (...
Meven Lennon-Bertrand's user avatar
2 votes

LEM, the halting problem, the curry-howard correspondence -> deep connection?

I'll just try and address some of the more basic points, I'll let others deal with the more technical details related to proof assistants (see Mario Carneiro's answer for example): Is it correct that ...
Julio Di Egidio - inactive's user avatar
2 votes

Natural deduction vs simply typed lambda calculus

The big picture is painted by the Curry-Howard isomorphism. If you make your question more specific and targeted, a less general answer might be possible.
Andrej Bauer's user avatar
  • 9,593
2 votes

Generic proof assistants/modularity of the proof assistants?

Both Metamath (and Metamath Zero) are naturally foundation generic. Metamath Like Isabelle, most of the active work done in Metamath is in just one theory (specifically set.mm uses ZFC). Nonetheless, ...
Jason Rute's user avatar
  • 8,960
2 votes

Generic proof assistants/modularity of the proof assistants?

I believe one "emerging proof assistant" along these lines is Andromeda. The theory of Andromeda is essentially an extensional dependent type theory with equality reflection, which can be ...
Mike Shulman's user avatar
  • 3,190
2 votes

Is there something special about weak head normal form used with proof assistants?

Note that weak head normal form is not important in all proof assistants. The HOLish systems (including Isabelle/HOL) implement a more-or-less simply typed lambda-calculus, and their kernels don't ...
Michael Norrish's user avatar

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