User loginNavigation 
Type TheoryMixedSite VarianceRoss Tate is calling for "Industry Endorsement" for his paper MixedSite Variance.
Abstract: Java introduced wildcards years ago. Wildcards were very expressive, and they were integral to updating the existing libraries to make use of generics. Unfortunately, wildcards were also complex and verbose, making them hard and inconvenient for programmers to adopt. Overall, while an impressive feature, wildcards are generally considered to be a failure. As such, many languages adopted a more restricted feature for generics, namely declarationsite variance, because designers believed its simplicity would make it easier for programmers to adopt. Indeed, declarationsite variance has been quite successful. However, it is also completely unhelpful for many designs, including many of those in the Java SDK. So, we have designed mixedsite variance, a careful combination of definitionsite and usesite variance that avoids the failings of wildcards. We have been working with JetBrains to put this into practice by incorporating it into the design of their upcoming language, Kotlin. Here we exposit our design, our rationale, and our experiences. Mention of it is also at Jetbrain's Kotlin blog. Dependent Types for JavaScriptDependent Types for JavaScript, by Ravi Chugh, David Herman, Ranjit Jhala:
Some good progress on inferring types for a very dynamic language. Explicit type declarations are placed in comments that start with "/*:". /*: xâˆ¶Top â†’ {Î½ âˆ£ite Num(x) Num(Î½) Bool(Î½)} */ function negate(x) { if (typeof x == "number") { return 0  x; } else { return !x; } } By naasking at 20130323 15:08  ObjectFunctional  Theory  Type Theory  128 comments  other blogs  29977 reads
How OCaml type checker works  or what polymorphism and garbage collection have in commonHow OCaml type checker works  or what polymorphism and garbage collection have in common
As usual with Oleg, there's a lot going on here. Personally, I see parallels with "lambda with letrec" and "callbypushvalue," although making the connection with the latter takes some squinting through some of Levy's work other than his CBPV thesis. Study this to understand OCaml type inference and/or MLF, or for insights into region typing, or, as the title suggests, for suggestive analogies between polymorphism and garbage collection. By Paul Snively at 20130310 16:25  Functional  Implementation  Type Theory  1 comment  other blogs  16621 reads
Records, sums, cases, and exceptions: Rowpolymorphism at workVideo: Records, sums, cases, and exceptions: Rowpolymorphism at work, Matthias Blume.
Found this to be an enjoyable and thorough overview of MLPolyR, a language created for a PL course that goes allout on various dimensions of row polymorphism, resulting in a small yet powerful language. (previously) By Manuel J. Simoni at 20121101 10:12  Implementation  Type Theory  4 comments  other blogs  17976 reads
Koka a function oriented language with effect inference
Koka extends the idea of using row polymorphism to encode an effect system and the relations between them. Daan Leijen is the primary researcher behind it and his research was featured previously on LtU, mainly on row polymorphism in the Morrow Language. So far there's no paper available on the language design, just the slides from a Lang.Next talk (which doesn't seem to have video available at Channel 9), but it's in the program for HOPE 2012. By Daniel Yokomizo at 20120816 05:40  Functional  Software Engineering  Type Theory  3 comments  other blogs  20636 reads
How to Make Ad Hoc Proof Automation Less Ad HocHow to Make Ad Hoc Proof Automation Less Ad Hoc
If you've ever toyed with Coq but run into the difficulties that many encounter in trying to construct robust, comprehensible proof scripts using tactics, which manipulate the proof state and can leave you with the "ground" of the proof rather than the "figure," if you will, in addition to being fragile in the face of change, you may wish to give this a read. It frankly never would have occurred to me to try to turn Ltac scripts into lemmas at all. This is much more appealing than most other approaches to the subject I've seen. By Paul Snively at 20120622 15:41  Functional  Implementation  Logic/Declarative  Type Theory  9 comments  other blogs  9741 reads
Tool Demo: ScalaVirtualized
Scala has always had a quite good EDSL story thanks to implicits, dot and pareninference, and methodsasoperators. Lately there are proposals to provide it with both macrosinthecamlp4sense and support for multistage programming. This paper goes into some depth on the foundations of the latter subject. By Paul Snively at 20120526 22:28  DSL  Implementation  MetaProgramming  ObjectFunctional  Scala  Semantics  Type Theory  login or register to post comments  other blogs  10607 reads
Programming as collaborative referenceProgramming as collaborative reference (extended abstract and slides) by everybody's favorite PLT tag team, Oleg and Chungchieh, from the Offthebeaten track workshop affiliated with POPL 2012:
By Manuel J. Simoni at 20120204 16:48  Paradigms  Type Theory  12 comments  other blogs  9664 reads
The Algebra of Data, and the Calculus of MutationKalani Thielen's The Algebra of Data, and the Calculus of Mutation is a very good explanation of ADTs, and also scratches the surfaces of Zippers:
(hat tip to Daniel Yokomizo, who used to be an LtU member...) By Manuel J. Simoni at 20120203 15:53  Teaching & Learning  Type Theory  11 comments  other blogs  12813 reads
Vellvm: Formalizing the LLVM Intermediate Representation for Verified Program TransformationsVellvm: Formalizing the LLVM Intermediate Representation for Verified Program Transformations by Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic, POPL 2012
This obviously represents huge progress in marrying the theoretical benefits of tools like Coq with the practical benefits of tools like LLVM. We can only hope that this spurs further development in practical certified software development. By Paul Snively at 20120128 15:57  Functional  Lambda Calculus  Semantics  Type Theory  16 comments  other blogs  13522 reads

Browse archivesActive forum topicsNew forum topics 
Recent comments
8 hours 19 min ago
1 week 4 days ago
2 weeks 59 min ago
2 weeks 9 hours ago
2 weeks 1 day ago
2 weeks 1 day ago
2 weeks 1 day ago
2 weeks 2 days ago
2 weeks 2 days ago
2 weeks 2 days ago