Jeremy Siek

508 followers -

Prof. at Indiana University Bloomington

Prof. at Indiana University Bloomington

508 followers

Jeremy's posts

Post has attachment

Public

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

semantics...

Post has attachment

Public

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

Public

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

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

Wait while more posts are being loaded