[Grace-core] Duck TYping at PoPL

[Andrew P. Black]

I've just listened to this presentation at PoPL.  I think that it's relevant to Grace, but don't pretend to understand the technical details.

See http://cseweb.ucsd.edu/~rchugh/research/nested/

system d :: nested refinement types

Nested Refinements: A Logic for Duck Typing
Ravi Chugh, Patrick M. Rondon, and Ranjit Jhala
POPL 2012 [ .pdf | tech report (arxiv) | .bib ] 

Programs written in dynamic languages make heavy use of features --- run-time type tests, value-indexed dictionaries, polymorphism, and higher-order functions --- that are beyond the reach of type systems that employ either purely syntactic or purely semantic reasoning. We present a core calculus, System D, that merges these two modes of reasoning into a single powerful mechanism of nested refinement types wherein the typing relation is itself a predicate in the refinement logic. System D coordinates SMT-based logical implication and syntactic subtyping to automatically typecheck sophisticated dynamic language programs. By coupling nested refinements with McCarthy's theory of finite maps, System D can precisely reason about the interaction of higher-order functions, polymorphism, and dictionaries. The addition of type predicates to the refinement logic creates a circularity that leads to unique technical challenges in the metatheory, which we solve with a novel stratification approach that we use to prove the soundness of System D.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailhost.cecs.pdx.edu/mailman/private/grace-core/attachments/20120126/cf201734/attachment.html>