6
$\begingroup$

I am an university student working on a thesis about λ-calculus. I'd like to know if there's any article or publication about proof assistant formalizations of the Bohm theorem ("any two normal forms in λ-calculus which are not ­­η-convertible are separable"), or more generally about Bohm trees and related topics, so that I can decide whether working on it or doing something else.

I've searched on different sites and archives (Coq library, Isabelle Archive of Formal Proofs, Mizar webpage, this StackExchange forum, the Coq Zulip chat, and I did some direct research on Google) but didn't find anything. Can you suggest any website or other resource where I might find them? Do you already know about any similar article or work?

Thanks in advance

Improve this question
$\endgroup$
1
  • $\begingroup$ I have also wondered about mechanising this result and my earlier searches also suggested that it hasn't been done. $\endgroup$
    – Michael Norrish
    Commented Feb 28, 2023 at 0:08

1 Answer 1

Reset to default
3
$\begingroup$

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 particular case where the meaningless terms you consider are the unsolvable ones, you get exactly the Böhm trees as normal forms.

This may seem quite convoluted, but it is arguably a good definition of Böhm trees (see the corresponding paper, the original definition of infinitary λ-calculi, the survey in the Barendregt-Manzonetto Satellite).

The formalization is available on Github.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.