Profile cover photo
Profile photo
Jeremy Siek
510 followers -
Prof. at Indiana University Bloomington
Prof. at Indiana University Bloomington

510 followers
About
Jeremy's posts

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\). \[
E...

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...

Post has attachment
The Publication Process in Programming Languages
There was an interesting discussion at the ACM SIGPLAN Meeting at POPL 2014 regarding the problems and potential solutions with the publication process within programming languages. The discussion centered around the problem that we primarily publish in con...

Post has attachment

Post has attachment
Wait while more posts are being loaded