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

510 followers
About
Posts

Post has attachment
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
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
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
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
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
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
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
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
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
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