Stream: Beginner Questions

Topic: Best practices for implementing object logics

Alex Nelson (Feb 10 2024 at 15:21):

I'm patching up Isabelle/Mizar to work with Isabelle2023, and I am wondering what are the best practices for implementing an object logic in Isabelle? (Usually there is great documentation for Isabelle, but this is the one department where it is lacking.)

Some random selection of the questions which come to mind:

• Is there an idiomatic way to implement "unit tests" to double check, e.g., the syntactic constructions are working as intended? (I know that we can prove results concerning the implementation, but just "quick example usage" type tests are helpful.)
• Are there expected metatheorems to prove various properties of the object logic?
• Are there idiomatic judgments to implement? Is there some expected "skeleton" which object logics should resemble?

(I asked this on the proof assistants stackexchange site, but that site seems to increasingly defunct...)

Last updated: Apr 28 2024 at 12:28 UTC