Entry Grossman:2000:STA from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Grossman:2000:STA,
  author =       "Dan Grossman and Greg Morrisett and Steve Zdancewic",
  title =        "Syntactic type abstraction",
  journal =      j-TOPLAS,
  volume =       "22",
  number =       "6",
  pages =        "1037--1080",
  year =         "2000",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Wed Jul 25 13:55:50 MDT 2001",
  bibsource =    "http://www.acm.org/pubs/toc/;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  URL =          "http://www.acm.org/pubs/articles/journals/toplas/2000-22-6/p1037-grossman/p1037-grossman.pdf;
                 http://www.acm.org/pubs/citations/journals/toplas/2000-22-6/p1037-grossman/",
  abstract =     "Software developers often structure programs in such a
                 way that different pieces of code constitute distinct
                 {\em principals}. Types help define the protocol by
                 which these principals interact. In particular, {\em
                 abstract types\/} allow a principal to make strong
                 assumptions about how well-typed clients use the
                 facilities that it provides. We show how the notions of
                 principals and type abstraction can be formalized
                 within a language. Different principals can know the
                 implementation of different abstract types. We use
                 additional syntax to track the flow of values with
                 abstract types during the evaluation of a program and
                 demonstrate how this framework supports syntactic
                 proofs (in the style of subject reduction) for
                 type-abstraction properties. Such properties have
                 traditionally required semantic arguments; using syntax
                 avoids the need to build a model and recursive types
                 for the language. We present various typed lambda
                 calculi with principals, including versions that have
                 mutable state and recursive types.",
  acknowledgement = ack-nhfb,
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  generalterms = "Languages; Security; Theory; Verification",
  keywords =     "operational semantics; parametricity; proof
                 techniques; syntactic proofs; type abstraction",
  subject =      "Software --- Software Engineering --- Software
                 Architectures (D.2.11): {\bf Information hiding};
                 Software --- Software Engineering --- Software
                 Architectures (D.2.11): {\bf Languages (e.g.,
                 description, interconnection, definition)}; Software
                 --- Programming Languages --- Formal Definitions and
                 Theory (D.3.1): {\bf Syntax}; Software --- Programming
                 Languages --- Formal Definitions and Theory (D.3.1):
                 {\bf Semantics}; Software --- Programming Languages ---
                 Language Constructs and Features (D.3.3): {\bf Abstract
                 data types}; Theory of Computation --- Logics and
                 Meanings of Programs --- Semantics of Programming
                 Languages (F.3.2): {\bf Operational semantics}; Theory
                 of Computation --- Logics and Meanings of Programs ---
                 Studies of Program Constructs (F.3.3): {\bf Type
                 structure}",
}

Related entries