Jeremy Siek

510 followers -

Prof. at Indiana University Bloomington

Prof. at Indiana University Bloomington

510 followers

Posts

Post has attachment

Public

**What do real numbers have in common with lambdas? and what does continuity have to do with it?**

Continuous functions over the real numbers As a high school student and undergraduate I learned in Calculus that real numbers sometimes require an infinite amount of information to explicitly describe, and continuous functions are smooth and unbroken, which...

Add a comment...

Post has attachment

Public

**Putting the Function back in Lambda**

Happy holidays! There’s nothing quite like curling up in a comfy chair on a rainy day and proving a theorem in your favorite proof assistant. Lately I’ve been interested in graph models of the \(\lambda\) -calculus, that is, models that represent a \(\lambd...

Add a comment...

Post has attachment

Public

**New revision of the semantics paper (POPL rejection, ESOP submission)**

My submission about declarative semantics to POPL was rejected. It's been a few weeks now, so I'm not so angry about it anymore. I've revised the paper and will be submitting it to ESOP this week. The main reason for rejection according to the reviewers was...

Add a comment...

Post has attachment

Public

**Comparing to Plotkin and Engeler's Set-theoretic Models of the Lambda Calculus**

On the plane ride back from ICFP last month I had a chance to re-read and better understand Plotkin’s Set-theoretical and other elementary models of the \(\lambda\) -calculus (Technical Report 1972, Theoretical Computer Science 1993) and to read, for the fi...

Add a comment...

Post has attachment

Public

**POPL submission, pulling together these blog posts on semantics!**

Last week I submitted a paper to POPL 2018 about the new kind of denotational semantics that I've been writing about in this blog, which I am now calling declarative semantics . I think this approach to semantics has the potential to replace operational sem...

Add a comment...

Post has attachment

Public

**Revisiting "well-typed programs cannot go wrong"**

Robin Milner proved that well-typed programs cannot go wrong in his 1978 paper A Theory of Type Polymorphism in Programming (Milner 1978) . That is, he defined a type system and denotational semantics for the Exp language (a subset of ML) and then proved ...

Add a comment...

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

Add a comment...

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

Add a comment...

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

Add a comment...

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

Add a comment...

Wait while more posts are being loaded