Skip to main content
8 votes
Accepted

Do we care about confluence because of unique normal forms?

I don't know what you mean by "practical", but confluence is very useful from the semantic point of view. Hopefully other people will be able to give you other answers from other points of view (for ...
Damiano Mazza's user avatar
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
5 votes

Moggi's computational metalanguage

It is an interesting problem to figure out what bothers the OP. First of all, it is not at all the case that the equation put forward by the OP says "different computations have the same value". For ...
Andrej Bauer's user avatar
  • 29.2k
3 votes

Why structural rules define the "smallest relation" satisfying the rules?

"Smallest relation with property $\mathscr{P}$" just means "subset of every relation with property $\mathscr{P}$" - thinking of a relation as a set of ordered pairs. Basically, we ...
Noah Schweber's user avatar
2 votes
Accepted

Moggi's computational metalanguage

I still don't quite understand what having a value means, but just considering the question of "can we give up the eta rule for monads", the answer is yes, this is an entirely reasonable thing to ...
Neel Krishnaswami's user avatar
2 votes

Operational semantics and denotational semantics and describing the behaviour and structure of programs

I am going to attempt an answer, or more precisely a clarification, but one should keep in mind that most ingredients of the question (semantics, operational, behavior, structure) do not have a clear ...
Beniamino Accattoli's user avatar
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
1 vote
Accepted

What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?

It took me a while to realize, but, at least for the standard $\lambda$-calculus, those two should actually coincide. I'm not sure if there's any reference to this (I'd like to see it if there is!), ...
paulotorrens's user avatar

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