SydneyTypes / PLATYPUS

Lunchtime type theory study group in Sydney
https://www.meetup.com/Sydney-Type-Theory
7 stars 3 forks source link

How do denotational, axiomatic and operational semantics relate to statics and dynamics in PFPL? #4

Open CMCDragonkai opened 8 years ago

CMCDragonkai commented 8 years ago

Question in the title ^!

thsutton commented 8 years ago

I think we see denotational and operational semantics in PFPL in the big-step and small-step dynamics described in the chapters, no?

CMCDragonkai commented 8 years ago

What pages are you referring to?

thsutton commented 8 years ago

Although I suppose "this other element of the same inductively defined set of objects" probably isn't what you mean by denotational semantics.

thsutton commented 8 years ago

Right, I'm crazy. What we're doing as "dynamics" is operational semantics.

SamRoberts commented 8 years ago

Denotational still seems clearly to be related to dynamics. And operational semantics basically is dynamics afaict. Axiomatic semantics is not obvious to me though: that pre/post stuff looks an awful lot like what a type system does.

thsutton commented 8 years ago

I'll try to form a more informed opinion tonight.

CMCDragonkai commented 6 years ago

@thsutton Have you formulated your informed opinion yet?

thsutton commented 6 years ago

No