6 votes
Accepted

Formalization of matching logic (logic behind K Framework)

There is a number of formalizations of matching logic in various proof assistants. I am a co-author of the first one in the following list; thus I have more insight into that one. I am not aware of ...
Jan Tušil's user avatar
2 votes

State machine classes with sub-exponentially growing model spaces

I believe that there are no reasonable model where the number of machines grow subexponentially, in the sense that either such a model would be remarkably not expressive, or would require huge ...
Rémi's user avatar
  • 262
1 vote

Formalization of matching logic (logic behind K Framework)

I'm currently at the end of my PhD thesis about the interoperability of semantics. That's the reason I'm studying the translation from the semantical framework K into the logical framework Dedukti. ...
Amélie Ledein's user avatar

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