This issue is to propose a working group for formalizing in Lean 4 the following topics:
- first-order logic over arbitrary (data) structures
- second-order logic and their interpretations (full, Henkin semantics)
- separation logic including novel connectives (G for finiteness of domain, @ for logical counter-part of virtual memory)
- weakest precondition/strongest postcondition calculi, Hoare's logic and Reynolds' logic
Currently I have a first experiment with using Claude and Lean, to speed up the development work. See also: https://codeberg.org/praalhans/seplogic
A community effort may allow us to have a formalization of the meta-theoretical results, that are useful later for certifying the implementation of proof checkers of various (program) logics.
This issue is to propose a working group for formalizing in Lean 4 the following topics:
Currently I have a first experiment with using Claude and Lean, to speed up the development work. See also: https://codeberg.org/praalhans/seplogic
A community effort may allow us to have a formalization of the meta-theoretical results, that are useful later for certifying the implementation of proof checkers of various (program) logics.