Profile cover photo
Profile photo
Jeremy Siek
Prof. at Indiana University Bloomington
Prof. at Indiana University Bloomington

Jeremy's posts

Post has attachment
Consolidation of the Denotational Semantics and an Application to Compiler Correctness
This is a two part post. The second part depends on the first. Part 1. Consolidation of the Denotational Semantics As a matter of expediency, I've been working with two different
versions of the intersection type system upon which the denotational

Post has attachment
The Take 3 Semantics, Revisited
In my post about intersection types as denotations , I conjectured that
the simple "take 3" denotational semantics is equivalent to an
intersection type system. I haven't settled that question per se, but
I've done something just as good, which is to show t...

Post has attachment
Sound wrt. Contextual Equivalence
The ICFP paper submission deadline kept me busy for much of February,
but now I'm back to thinking about the simple denotational semantics of the lambda calculus. In previous posts I showed that this semantics
is equivalent to standard operational semantics...

Post has attachment
On the Meaning of Casts and Blame for Gradual Typing
Gradually typed languages enable programmers to choose which parts of
their programs are statically typed and which parts are dynamically
typed. Thus, gradually typed languages perform some type checking at
compile time and some type checking at run time. W...

Post has attachment
Completeness of Intersection Types wrt. an Applied CBV Lambda Calculus
I'm still quite excited about the simple denotational semantics and
looking forward to applying it to the semantics of gradually typed
languages. However, before building on it I'd like to make sure it's
correct. Recall that I proved soundness of the simple...

Post has attachment
Intersection Types as Denotations
In my previous post I described a simple denotational semantics for
the CBV lambda calculus in which the meaning of a \(\lambda\) function
is a set of tables. For example, here is a glimpse at some of the
tables in the meaning of \(\lambda x. x+2\). \[

Post has attachment
Take 3: Application with Subsumption for Den. Semantics of Lambda Calculus
Alan Jeffrey tweeted the following in reply to the previous post: @jeremysiek wouldn't it be easier to change the defn of application to be ⟦MN⟧σ = { W | T ∈ ⟦M⟧σ, V ∈ ⟦N⟧σ, (V′,W) ∈ T, V′ ⊆ V }? The idea is that, for higher order functions, if the function...

Post has attachment
Take 2: Graph of Tables for the Denotational Semantics of the Lambda Calculus
In the previous post, the denotational semantics I gave for the lambda calculus could not deal with
self application, such as the program
(\lambda f. f\;f)\;(\lambda g. 42)
whose result should be \(42\).
The problem was that I defined function value...

Post has attachment
Simple Denotational Semantics for the Lambda Calculus, Pω Revisited?
I've been trying to understand Dana Scott's \(P_{\omega}\) and \(D_{\infty}\) models of
the lambda calculus, as well as a couple large Coq formalizations of domain theory,
and in the process have come up with an extraordinarily simple
denotational semantics...

Post has attachment
Denotational Semantics of IMP without Fixed Points
It has been too long since I wrote a blog post!
Needless to say, parenthood, teaching, research, services, and my wonderful graduate
students and post-docs have been keeping me busy.
But with the Fall 2016 semester winding down I can sneak away for a bit an...
Wait while more posts are being loaded