Sign up ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

I'm wondering if anyone knows of a formalization (even limited) of any part of finite model theory in any of the major proof assistants. (I'm most familiar with Coq, but Isabelle, Agda, etc. would acceptable.)

Especially of interest would be any of the results in descriptive complexity.

share|cite|improve this question

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.