Jeremy Siek

510 followers -

Prof. at Indiana University Bloomington

Prof. at Indiana University Bloomington

510 followers

Jeremy's posts

Post has attachment

Public

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

Public

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

Public

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

Public

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

Public

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

Public

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

Public

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

Public

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

Public

Post has attachment

Public

Wait while more posts are being loaded