proposal.bib

% This file was created with JabRef 2.9.2.
% Encoding: Cp1252

@ARTICLE{Cervesato+Scedrov:IC09,
  author = {Cervesato, Iliano and Scedrov, Andre},
  title = {Relating State-Based and Process-Based Concurrency through Linear Logic},
  journaltitle = {Information and Computation},
  editor = {Mints, Grigori and de Paiva, Val{\'e}ria and de Queiroz, Ruy},
  date = {2009-10},
  volume = {207},
  number = {10},
  pages = {1044--1077},
  issuetitle = {Special Issue},
  issuesubtitle = {13th Workshop on Logic, Language, Information, and Computation (WoLLIC 2006)},
  issn = {0890-5401},
  doi = {10.1016/j.ic.2008.11.006}
}

@INPROCEEDINGS{Miller:ELP92,
  author = {Miller, Dale},
  title = {The $\pi$-Calculus as a Theory in Linear Logic},
  subtitle = {Preliminary Results},
  crossref = {ELP92},
  date = {1992},
  pages = {242--264},
  doi = {10.1007/3-540-56454-3_13}
}

@PROCEEDINGS{ELP92,
  editor = {Lamma, Evelina and Mello, Paola},
  title = {Extensions of Logic Programming, Third International Workshop,
               ELP'92, Proceedings},
  venue = {Bologna, Italy},
  eventdate = {1992-02-26/1992-02-28},
  xdata = {LNCS},
  volume = {660},
  date = {1993},
  isbn = {3-540-56454-3},
  doi = {10.1007/3-540-56454-3}
}

@ARTICLE{Andreoli:APAL01,
  author = {Andreoli, Jean-Marc},
  title = {Focussing and Proof Construction},
  journaltitle = {Annals of Pure and Applied Logic},
  date = {2001-01-15},
  volume = {107},
  number = {1--3},
  pages = {131--163},
  issn = {0168-0072},
  doi = {10.1016/S0168-0072(00)00032-4}
}

@UNPUBLISHED{Toninho+:coind13,
  author = {Toninho, Bernardo and Caires, Lu{\'i}s and Pfenning, Frank},
  title = {Coinductive Session Types in Higher-Order Communication Centric Programs},
  date = {2013},
  pubstate = {submitted},
  url = {http://www.cs.cmu.edu/~fp/papers/coind13.pdf}
}

@INPROCEEDINGS{Pfenning:APLAS04,
  crossref = {APLAS04},
  author = {Pfenning, Frank},
  title = {Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk)},
  pages = {196},
  doi = {10.1007/978-3-540-30477-7_13}
}

@PROCEEDINGS{APLAS04,
  editor = {Chin, Wei-Ngan},
  title = {Programming Languages and Systems: Second Asian Symposium, APLAS 2004},
  date = {2004},
  venue = {Taipei, Taiwan},
  eventdate = {2004-11-04/2004-11-06},
  xdata = {LNCS},
  volume = {3302},
  isbn = {3-540-23724-0}
}

@INPROCEEDINGS{Pfenning+Simmons:LICS09,
  crossref = {LICS09},
  author = {Pfenning, Frank and Simmons, Robert J.},
  title = {Substructural Operational Semantics as Ordered Logic Programming},
  pages = {101--110},
  doi = {10.1109/LICS.2009.8}
}

@PROCEEDINGS{LICS09,
  editor = {Pitts, Andrew M.},
  title = {Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009},
  date = {2009},
  venue = {Los Angeles},
  eventdate = {2009-08-11/2009-08-14},
  xdata = {IEEE},
  isbn = {978-0-7695-3746-7}
}

@XDATA{IEEE,
  publisher = {IEEE Computer Society}
}

@ARTICLE{Lambek:AMM58,
  author = {Lambek, Joachim},
  title = {The Mathematics of Sentence Structure},
  journaltitle = {The American Mathematical Monthly},
  date = {1958-03},
  volume = {65},
  number = {3},
  pages = {154--170},
  issn = {0002-9890},
  doi = {10.2307/2310058}
}

@ARTICLE{Andreoli:JLC92,
  author = {Andreoli, Jean-Marc},
  title = {Logic Programming with Focusing Proofs in Linear Logic},
  editor = {Gabbay, Dov M.},
  journaltitle = {Journal of Logic and Computation},
  date = {1992},
  volume = {2},
  number = {3},
  pages = {297--347},
  issn = {0955-792X},
  doi = {10.1093/logcom/2.3.297},
  abstract = {The deep symmetry of linear logic makes it suitable for providing abstract models of computation, free from implementation details which are, by nature, oriented and non-symmetrical.  I propose here one such model, in the area of logic programming, where the basic computational principle is Computation = Proof search.  Proofs considered here are those of the Gentzen style sequent calculus for linear logic.  However, proofs in this system may be redundant, in that two proofs can be syntactically different although identical up to some irrelevant reordering or simplification of the applications of the inferences rules.  This leads to an intractable proof search where the search procedure is forced to make costly choices which turn out to be irrelevant.  To overcome this problem, a subclass of proofs, called the `focusing' proofs, which is both complete (any derivable formula in linear logic has a focusing proof) and tractable (many irrelevant choices in the search are eliminated when aimed at focusing proofs) is identified.  The main constraint underlying the specification of focusing proofs has been to preserve the symmetry of linear logic, which is its most salient feature.  In particular, dual connectives have dual properties with respect to focusing proofs.  Then, a programming language, called LinLog, consisting of a fragment of linear logic, in which focusing proofs have a more compact form, is presented.  LinLog deals with formulae which have a syntax similar to the of the definite clauses and goals of Horn logic, but the crucial difference here is that it allows clauses with multiple atoms in the head, connected by the `par' (multiplicative disjunction).  It is then shown that the syntactic restriction induced by LinLog is not performed at the cost of any expressive power: a mapping from full linear logic to LinLog, preserving focusing proofs, and analogous to the normalization to clausal form for classical logic, is presented.}
}

@TECHREPORT{Barber:ECS96,
  author = {Barber, Andrew},
  title = {Dual Intuitionistic Linear Logic},
  institution = {Department of Computer Science, University of Edinburgh},
  date = {1996-09},
  number = {ECS-LFCS-96-347},
  location = {Edinburgh},
  abstract = {We present a new intuitionistic linear logic, Dual Intuitionistic Linear Logic, designed to reflect the motivation of exponentials as translations of intuitionistic types, and provide it with a term calculus, proving associated standard type-theoretic results.  We give a sound and complete categorical semantics for the type-system, and consider the relationship of the new type-theory to the more familiar presentation found for example in ``A term calculus for intuitionistic linear logic'' by Benton et al.}
}

@INPROCEEDINGS{Toninho+:PPDP11,
  author = {Toninho, Bernardo and Caires, Lu{\'i}s and Pfenning, Frank},
  title = {Dependent Session Types via Intuitionistic Linear Type Theory},
  crossref = {PPDP11},
  pages = {161--172},
  doi = {10.1145/2003476.2003499}
}

@MISC{Pfenning:816Identity,
  author = {Pfenning, Frank},
  title = {Identity and Inversion},
  date = {2012-02-13},
  type = {\autocap{l}ecture notes},
  howpublished = {\autocap{o}nline},
  url = {http://www.cs.cmu.edu/~fp/courses/15816-s12/lectures/08-inversion.pdf}
}

@MISC{Pfenning:816,
  author = {Pfenning, Frank},
  title = {Linear Logic},
  date = {2012},
  type = {\autocap{l}ecture notes},
  howpublished = {\autocap{o}nline},
  url = {http://www.cs.cmu.edu/~fp/courses/15816-s12/schedule.html}
}

@XDATA{ACM,
  publisher = {ACM Press},
  location = {New York}
}

@PROCEEDINGS{PPDP11,
  editor = {Schneider-Kamp, Peter and Hanus, Michael},
  title = {Proceedings of the 13th International ACM SIGPLAN Conference
               on Principles and Practice of Declarative Programming},
  date = {2011},
  venue = {Odense, Denmark},
  eventdate = {2011-07-20/2011-07-22},
  xdata = {ACM},
  isbn = {978-1-4503-0776-5}
}

@INPROCEEDINGS{Caires+Pfenning:CONCUR10,
  crossref = {CONCUR10},
  author = {Caires, Lu{\'i}s and Pfenning, Frank},
  title = {Session Types as Intuitionistic Linear Propositions},
  pages = {222--236},
  doi = {10.1007/978-3-642-15375-4_16}
}

@XDATA{Springer,
  publisher = {Springer},
  location = {Heidelberg and Berlin}
}

@XDATA{LNCS,
  series = {Lecture Notes in Computer Science},
  xdata = {Springer}
}

@PROCEEDINGS{CONCUR10,
  editor = {Gastin, Paul and Laroussinie, Fran\c{c}ois},
  title = {CONCUR 2010 - Concurrency Theory, 21th International Conference, Proceedings},
  date = {2010},
  venue = {Paris},
  eventdate = {2010-08-31/2010-09-03},
  xdata = {LNCS},
  volume = {6269},
  isbn = {978-3-642-15374-7},
  doi = {10.1007/978-3-642-15375-4}
}

@INPROCEEDINGS{Honda:CONCUR93,
  crossref = {CONCUR93},
  author = {Honda, Kohei},
  title = {Types for Dyadic Interaction},
  pages = {509--523},
  doi = {10.1007/3-540-57208-2_35}
}

@PROCEEDINGS{CONCUR93,
  editor = {Best, Eike},
  title = {4th International Conference on Concurrency Theory},
  venue = {Hildesheim, Germany},
  eventdate = {1993-08-23/1993-08-26},
  xdata = {LNCS},
  volume = {715},
  date = {1993},
  isbn = {3-540-57208-2},
  doi = {10.1007/3-540-57208-2}
}

@TECHREPORT{Chang+:CMU03,
  author = {Chang, Bor-Yuh Evan and Chaudhuri, Kaustuv and Pfenning, Frank},
  title = {A Judgmental Analysis of Linear Logic},
  institution = {Carnegie Mellon University, Computer Science Department},
  date = {2003-04},
  number = {CMU-CS-03-131R},
  location = {Pittsburgh},
  note = {\autocap{r}evised December 2003},
  abstract = {We reexamine the foundations of linear logic, developing a system of natural deduction following Martin-L{\"o}f's separation of judgments from propositions.  Our construction yields a clean and elegant formulation that accounts for a rich set of multiplicative, additive, and exponential connectives, extending dual intuitionistic linear logic but differing from both classical linear logic and Hyland and de Paiva's full intuitionistic linear logic.  We also provide a corresponding sequent calculus that admits a simple proof of the admissibility of cut by a single structural induction.  Finally, we show how to interpret classical linear logic (with or without the MIX rule) in our system, employing a form of double-negation translation.}
}

@TECHREPORT{Colmerauer+:73,
  author = {Colmerauer, Alain and Kanoui, Henry and Roussel, Philippe and Pasero, Robert},
  title = {Un Syst{\`e}me de Communication Homme-Machine en Fran\c{c}ais},
  institution = {Groupe de recherche en Intelligence Artificielle},
  location = {Marseille},
  type = {\autocap{r}apport de recherche},
  date = {1973},
  hyphenation = {french}
}

@ARTICLE{Debray+Warren:TOPLAS89,
  author = {Debray, Saumya K. and Warren, David S.},
  title = {Functional Computations in Logic Programs},
  journaltitle = {ACM Transactions on Programming Languages and Systems},
  volume = {11},
  number = {3},
  date = {1989-07},
  pages = {451--481},
  doi = {10.1145/65979.65984}
}

@ARTICLE{Gentzen:MZ35,
  author = {Gentzen, Gerhard},
  title = {Untersuchungen {\"u}ber das logische {Schlie{\ss}en}},
  journaltitle = {Mathematische Zeitschrift},
  date = {1935},
  volume = {39},
  number = {1},
  pages = {176--210, 405--431},
  hyphenation = {german},
  related = {Szabo:69},
  relatedstring = {English translation in}
}

@BOOK{Szabo:69,
  author = {Gentzen, Gerhard},
  editor = {Szabo, Manfred E.},
  title = {The Collected Papers of {Gerhard} {Gentzen}},
  publisher = {North-Holland},
  location = {Amsterdam},
  date = {1969}
}

@ARTICLE{Girard:TCS87,
  author = {Girard, Jean-Yves},
  title = {Linear Logic},
  editor = {Nivat, Maurice and Paterson, Matthew S.},
  journaltitle = {Theoretical Computer Science},
  date = {1987},
  volume = {50},
  number = {1},
  pages = {1--102},
  issn = {0304-3975},
  doi = {10.1016/0304-3975(87)90045-4},
  abstract = {The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality ``of course'' which has the meaning of a reaffirmation.  Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.}
}

@INPROCEEDINGS{Hanus:Ganzinger13,
  author = {Hanus, Michael},
  title = {Functional Logic Programming},
  subtitle = {From Theory to {Curry}},
  booktitle = {Programming Logics},
  booksubtitle = {Essays in Memory of {Harald} {Ganzinger}},
  date = {2013},
  volume = {7797},
  series = {LNCS},
  pages = {123--168},
  publisher = {Springer},
  timestamp = {2013.09.24}
}

@ARTICLE{Hodas+Miller:IC94,
  author = {Hodas, Joshua S. and Miller, Dale},
  title = {Logic Programming in a Fragment of Intuitionistic Linear Logic},
  editor = {Kahn, Gilles},
  journaltitle = {Information and Computation},
  date = {1994-05},
  volume = {110},
  number = {2},
  issuetitle = {Special Conference Issue},
  issuesubtitle = {1991 {IEEE} Symposium on Logic in Computer Science},
  pages = {327--365},
  doi = {10.1006/inco.1994.1036},
  issn = {0890-5401}
}

@INBOOK{Howard:Curry80,
  author = {Howard, William A.},
  title = {The Formulae-as-Types Notion of Construction},
  pages = {479--490},
  editor = {Seldin, Jonathan P. and Hindley, J. Roger},
  booktitle = {To {H.B.\ Curry}},
  booksubtitle = {Essays on Combinatory Logic, Lambda Calculus, and Formalism},
  date = {1980},
  publisher = {Academic Press},
  location = {Boston}
}

@INPROCEEDINGS{Kowalski:IFIP74,
  author = {Kowalski, Robert},
  title = {Predicate Logic as Programming Language},
  booktitle = {Proceedings of the IFIP Congress},
  year = {1974},
  pages = {569--574},
  publisher = {North-Holland},
  location = {Amsterdam}
}


@INPROCEEDINGS{Lopez+:PPDP05,
  author = {L{\'o}pez, Pablo and Pfenning, Frank and Polakow, Jeff and Watkins, Kevin},
  title = {Monadic Concurrent Linear Logic Programming},
  editor = {Barahona, Pedro and Felty, Amy P.},
  booktitle = {Principles and Practice of Declarative Programming},
  booktitleaddon = {Proceedings of the 7th International ACM SIGPLAN Conference},
  eventdate = {2005-07-11/2005-07-13},
  venue = {Lisbon, Portugal},
  date = {2005},
  pages = {35--46},
  publisher = {ACM Press},
  location = {New York}
}

@BOOK{Martin-Lof:84,
  title = {Intuitionistic Type Theory},
  publisher = {Bibliopolis},
  year = {1984},
  author = {Martin-L{\"o}f, Per},
  timestamp = {2013.10.04}
}

@INCOLLECTION{Martin-Lof:LMPS80,
  author = {Martin-L{\"o}f, Per},
  title = {Constructive Mathematics and Computer Programming},
  booktitle = {Logic, Methodology and Philosophy of Science {VI}},
  publisher = {North-Holland},
  location = {Amsterdam},
  year = {1980},
  pages = {153--175}
}

@ARTICLE{Miller+:PAL91,
  author = {Miller, Dale and Nadathur, Gopalan and Pfenning, Frank and Scedrov, Andre},
  title = {Uniform Proofs as a Foundation for Logic Programming},
  editor = {Kozen, Dexter},
  journaltitle = {Annals of Pure and Applied Logic},
  date = {1991},
  volume = {51},
  number = {1--2},
  issuetitle = {Selected papers from the Second Annual {IEEE} Symposium on Logic in Computer Science},
  pages = {125--157},
  doi = {10.1016/0168-0072(91)90068-W},
  issn = {0168-0072},
  abstract = {A proof-theoretic characterization of logical languages that form suitable bases for Prolog-like programming languages is provided.  This characterization is based on the principle that the declarative meaning of a logic program, provided by provability in a logical system, should coincide with its operational meaning, provided by interpreting logical connectives as simple and fixed search instructions.  The operational semantics is formalized by the identification of a class of cut-free sequent proofs called uniform proofs.  A uniform proof is one that can be found by a goal-directed search that respects the interpretation of the logical connectives as search instructions.  The concept of a uniform proof is used to define the notion of an abstract logic programming language, and it is shown that first-order and higher-order Horn clauses with classical provability are examples of such a language.  Horn clauses are then generalized to hereditary Harrop formulas and it is shown that first-order and higher-order versions of this new class of formulas are also abstract logic programming languages if the inference rules are those of either intuitionistic or minimal logic.  The programming language significance of the various generalizations to first-order Horn clauses is briefly discussed.}
}

@PROCEEDINGS{TLDI12,
  editor = {Pierce, Benjamin C.},
  title = {Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation},
  date = {2012},
  venue = {Philadelphia},
  eventdate = {2012-01-28},
  publisher = {ACM Press},
  isbn = {978-1-4503-1120-5}
}

@INPROCEEDINGS{Caires+:TLDI12,
  crossref = {TLDI12},
  author = {Caires, Lu{\'i}s and Pfenning, Frank and Toninho, Bernardo},
  title = {Towards Concurrent Type Theory},
  pages = {1--12},
  doi = {10.1145/2103786.2103788}
}

@INPROCEEDINGS{Caires+:ESOP13,
  author = {Caires, Lu{\'i}s and P{\'e}rez, Jorge A. and Pfenning, Frank and Toninho, Bernardo},
  title = {Behavioral Polymorphism and Parametricity in Session-Based Communication},
  crossref = {ESOP13},
  pages = {330--349},
  doi = {10.1007/978-3-642-37036-6_19}
}

@INPROCEEDINGS{Toninho+:ESOP13,
  author = {Toninho, Bernardo and Caires, Lu{\'i}s and Pfenning, Frank},
  title = {Higher-Order Processes, Functions, and Sessions},
  subtitle = {A Monadic Integration},
  crossref = {ESOP13},
  pages = {350--369},
  doi = {10.1007/978-3-642-37036-6_20}
}

@PROCEEDINGS{ESOP13,
  editor = {Felleisen, Matthias and Gardner, Philippa},
  title = {Programming Languages and Systems - 22nd European Symposium
               on Programming, ESOP 2013, Held as Part of the European
               Joint Conferences on Theory and Practice of Software, ETAPS
               2013. Proceedings.},
  date = {2013},
  venue = {Rome},
  eventdate = {2013-03-16/2013-03-24},
  xdata = {LNCS},
  volume = {7792},
  isbn = {978-3-642-37035-9},
  doi = {10.1007/978-3-642-37036-6}
}

@INPROCEEDINGS{DeYoung+:CSL12,
  author = {DeYoung, Henry and Caires, Lu{\'i}s and Pfenning, Frank and Toninho, Bernardo},
  title = {Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication},
  crossref = {CSL12},
  pages = {228--242},
  doi = {10.4230/LIPIcs.CSL.2012.228}
}

@XDATA{LIPIcs,
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik},
  series    = {LIPIcs}
}

@PROCEEDINGS{CSL12,
  editor = {C{\'e}gielski, Patrick and Durand, Arnaud},
  title = {Computer Science Logic (CSL'12) - 26th International Workshop/21st
               Annual Conference of the EACSL},
  date = {2012},
  eventdate = {2012-09-03/2012-09-06},
  venue = {Fontainebleau, France},
  xdata = {LIPIcs},
  volume = {16},
  isbn = {978-3-939897-42-2},
  issn = {1868-8969}
}

@BOOK{Prawitz:65,
  author = {Prawitz, Dag},
  title = {Natural Deduction},
  subtitle = {A Proof-Theoretical Study},
  date = {1965},
  publisher = {Almqvist \& Wiksell},
  location = {Stockholm}
}

@ARTICLE{Sabry+Felleisen:LASC93,
  author = {Sabry, Amr and Felleisen, Matthias},
  title = {Reasoning about Programs in Continuation-Passing Style},
  journaltitle = {{LISP} and Symbolic Computation},
  date = {1993},
  volume = {6},
  pages = {289--360},
  number = {3--4},
  issn = {0892-4635},
  doi = {10.1007/BF01019462},
  abstract = {Plotkin's $\lambda_\nu$-calculus for call-by-value programs is weaker than the $\lambda\beta\eta$-calculus for the same programs in continuation-passing style (CPS). To identify the call-by-value axioms that correspond to $\beta\eta$ on CPS terms, we define a new CPS transformation and an inverse mapping, both of which are interesting in their own right. Using the new CPS transformation, we determine the precise language of CPS terms closed under $\beta\eta$-transformations, as well as the call-by-value axioms that correspond to the so-called administrative $\beta\eta$-reductions on CPS terms. Using the inverse mapping, we map the remaining $\beta$ and $\eta$ equalities on CPS terms to axioms on call-by-value terms. On the pure (constant free) set of $\Lambda$-terms, the resulting set of axioms is equivalent to Moggi's computational $\lambda$-calculus. If the call-by-value language includes the control operators abort and call-with-current-continuation, the axioms are equivalent to an extension of Felleisen et al.'s $\lambda_\nu$-C-calculus and to the equational subtheory of Talcott's logic IOCC.}
}

@ARTICLE{Simmons+Pfenning:HOSC11,
  author = {Simmons, Robert J. and Pfenning, Frank},
  title = {Logical Approximation for Program Analysis},
  journaltitle = {Higher-Order and Symbolic Computation},
  date = {2011},
  volume = {24},
  pages = {41--80},
  number = {1--2},
  xdata = {Springer},
  issn = {1388-3690},
  doi = {10.1007/s10990-011-9071-2}
}

@BOOK{Book+Otto:SRS93,
  author = {Book, Ronald V. and Otto, Friedrich},
  title = {String-Rewriting Systems},
  date = {1993},
  series = {Text and Monographs in Computer Science},
  xdata = {Springer},
  isbn = {978-1-4613-9773-1},
  doi = {10.1007/978-1-4613-9771-7_3}
}

@INPROCEEDINGS{Polakow+Pfenning:MFPS99,
  crossref = {MFPS99},
  author = {Polakow, Jeff and Pfenning, Frank},
  title = {Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic},
  pages = {449--466},
  doi = {10.1016/S1571-0661(04)80088-4}
}

@PROCEEDINGS{MFPS99,
  editor = {Scedrov, Andre and Jung, Achim},
  title = {Proceedings of the 15th Conference on Mathematical Foundations of Programming Semantics},
  date = {1999},
  venue = {New Orleans, Louisiana},
  eventdate = {1999-04},
  xdata = {ENTCS},
  volume = {20}
}

@XDATA{ENTCS,
  series = {Electronic Notes in Theoretical Computer Science}
}

@PHDTHESIS{Simmons:CMU12,
  author = {Simmons, Robert J.},
  title = {Substructural Logical Specifications},
  school = {Carnegie Mellon University},
  date = {2012-11-14}
}

@PHDTHESIS{Schack-Nielsen:ITU11,
  author = {Schack-Nielsen, Anders},
  title = {Implementing Substructural Logical Frameworks},
  school = {IT University of Copenhagen},
  year = {2011}
}

@INPROCEEDINGS{Schack-Nielsen+Schuermann:IJCAR08,
  author = {Schack-Nielsen, Anders and Sch{\"u}rmann, Carsten},
  title = {{Celf}},
  subtitle = {A Logical Framework for Deductive and Concurrent Systems (System Description)},
  booktitle = {Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'08)},
  date = {2008},
  pages = {320--326},
  publisher = {Springer LNCS 5195}
}

@INPROCEEDINGS{Simmons+Zerny:LICS13,
  author = {Simmons, Robert J. and Zerny, Ian},
  title = {A Logical Correspondence between Natural Semantics and Abstract Machines},
  editor = {Kupferman, Orna},
  booktitle = {Logic in Computer Science},
  booktitleaddon = {Proceedings of the 28th Annual {ACM}/{IEEE} Symposium},
  date = {2013},
  venue = {New Orleans, LA},
  eventdate = {2013-06-25/2013-06-28}
}

@TECHREPORT{Watkins+:CMU02,
  author = {Watkins, Kevin and Cervesato, Iliano and Pfenning, Frank and Walker, David},
  title = {A Concurrent Logical Framework {I}},
  subtitle = {Judgments and Properties},
  date = {2002-03},
  institution = {Department of Computer Science, Carnegie Mellon University},
  number = {CMU-CS-2002-101},
  location = {Pittsburgh},
  note = {\autocap{r}evised May 2003}
}

@TECHREPORT{Cervesato+:CMU02,
  author = {Cervesato, Iliano and Pfenning, Frank and Walker, David and Watkins, Kevin},
  title = {A Concurrent Logical Framework {II}},
  subtitle = {Examples and Applications},
  date = {2002-03},
  institution = {Department of Computer Science, Carnegie Mellon University},
  number = {CMU-CS-2002-102},
  location = {Pittsburgh},
  note = {\autocap{r}evised May 2003}
}

@ARTICLE{Wright+Felleisen:IC94,
  author = {Wright, Andrew K. and Felleisen, Matthias},
  title = {A Syntactic Approach to Type Soundness},
  journaltitle = {Information and Computation},
  date = {1994},
  volume = {115},
  number = {1},
  pages = {38--94},
  doi = {10.1006/inco.1994.1093},
  issn = {0890-5401},
  abstract = {We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems.  The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics.  The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features.  We illustrate the technique with a type soundness theorem for the core of Standard ML, which includes the first type soundness proof for polymorphic exceptions and continuations.}
}

@comment{jabref-meta: selector_publisher:}

@comment{jabref-meta: selector_author:}

@comment{jabref-meta: selector_journal:}

@comment{jabref-meta: selector_keywords:}