publications: - title: "Harmony: The Art of Reconciliation" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2005" doi: "http://dx.doi.org/10.1007/11580850_1" links: doi: "http://dx.doi.org/10.1007/11580850_1" tags: - "C++" researchr: "https://researchr.org/publication/Pierce05" cites: 0 citedby: 0 pages: "1" booktitle: "Trustworthy Global Computing, International Symposium, TGC 2005, Edinburgh, UK, April 7-9, 2005, Revised Selected Papers" editor: - name: "Rocco De Nicola" link: "https://researchr.org/alias/rocco-de-nicola" - name: "Davide Sangiorgi" link: "https://researchr.org/alias/davide-sangiorgi" volume: "3705" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-30007-4" kind: "inproceedings" key: "Pierce05" - title: "Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem" author: - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Michael B. Greenwald" link: "https://researchr.org/alias/michael-b.-greenwald" - name: "Jonathan T. Moore" link: "https://researchr.org/alias/jonathan-t.-moore" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Alan Schmitt" link: "https://researchr.org/alias/alan-schmitt" year: "2007" doi: "http://doi.acm.org/10.1145/1232420.1232424" abstract: "We propose a novel approach to the view-update problem for tree-structured data: a domain-specific programming language in which all expressions denote bidirectional transformations on trees. In one direction, these transformations—dubbed lenses—map a concrete tree into a simplified abstract view; in the other, they map a modified abstract view, together with the original concrete tree, to a correspondingly modified concrete tree. Our design emphasizes both robustness and ease of use, guaranteeing strong well-behavedness and totality properties for well-typed lenses. We begin by identifying a natural space of well-behaved bidirectional transformations over ar- bitrary structures, studying definedness and continuity in this setting. We then instantiate this semantic framework in the form of a collection of lens combinators that can be assembled to de- scribe bidirectional transformations on trees. These combinators include familiar constructs from functional programming (composition, mapping, projection, conditionals, recursion) together with some novel primitives for manipulating trees (splitting, pruning, merging, etc.). We illustrate the expressiveness of these combinators by developing a number of bidirectional list-processing trans- formations as derived forms. An extended example shows how our combinators can be used to define a lens that translates between a native HTML representation of browser bookmarks and a generic abstract bookmark format." links: doi: "http://doi.acm.org/10.1145/1232420.1232424" tags: - "programming languages" - "bidirectional transformation" - "translation" - "data-flow language" - "generic programming" - "transformation language" - "composition" - "functional programming" - "language design" - "data-flow programming" - "data-flow" - "C++" - "programming" - "design" - "systematic-approach" - "transformation" - "program transformation" - "domain-specific language" researchr: "https://researchr.org/publication/FosterGMPS07" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "29" number: "3" pages: "17" kind: "article" key: "FosterGMPS07" - title: "Faithful Ideal Models for Recursive Polymorphic Types" author: - name: "Martín Abadi" link: "http://users.soe.ucsc.edu/~abadi/home.html" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Gordon D. Plotkin" link: "https://researchr.org/alias/gordon-d.-plotkin" year: "1991" tags: - "C++" researchr: "https://researchr.org/publication/AbadiPP91" cites: 0 citedby: 0 journal: "Int. J. Found. Comput. Sci." volume: "2" number: "1" pages: "1-21" kind: "article" key: "AbadiPP91" - title: "Exploiting Schemas in Data Synchronization" author: - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Michael B. Greenwald" link: "https://researchr.org/alias/michael-b.-greenwald" - name: "Christian Kirkegaard" link: "https://researchr.org/alias/christian-kirkegaard" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Alan Schmitt" link: "https://researchr.org/alias/alan-schmitt" year: "2005" doi: "http://dx.doi.org/10.1007/11601524_3" links: doi: "http://dx.doi.org/10.1007/11601524_3" tags: - "synchronization" - "XML" - "XML Schema" - "data-flow" - "C++" researchr: "https://researchr.org/publication/FosterGKPS05" cites: 0 citedby: 0 pages: "42-57" booktitle: "Database Programming Languages, 10th International Symposium, DBPL 2005, Trondheim, Norway, August 28-29, 2005, Revised Selected Papers" editor: - name: "Gavin M. Bierman" link: "https://researchr.org/alias/gavin-m.-bierman" - name: "Christoph Koch" link: "https://researchr.org/alias/christoph-koch" volume: "3774" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-30951-9" kind: "inproceedings" key: "FosterGKPS05" - title: "Linguistic foundations for bidirectional transformations: invited tutorial" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2012" doi: "http://doi.acm.org/10.1145/2213556.2213568" links: doi: "http://doi.acm.org/10.1145/2213556.2213568" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pods/Pierce12" researchr: "https://researchr.org/publication/Pierce12-1" cites: 0 citedby: 0 pages: "61-64" booktitle: "Proceedings of the 31st ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2012, Scottsdale, AZ, USA, May 20-24, 2012" editor: - name: "Michael Benedikt" link: "https://researchr.org/alias/michael-benedikt" - name: "Markus Krötzsch" link: "https://researchr.org/alias/markus-kr%C3%B6tzsch" - name: "Maurizio Lenzerini" link: "https://researchr.org/alias/maurizio-lenzerini" publisher: "ACM" isbn: "978-1-4503-1248-6" kind: "inproceedings" key: "Pierce12-1" - title: "A Theory of Information-Flow Labels" author: - name: "Benoît Montagu" link: "https://researchr.org/alias/beno%C3%AEt-montagu" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Randy Pollack" link: "https://researchr.org/alias/randy-pollack" year: "2013" doi: "http://dx.doi.org/10.1109/CSF.2013.8" links: doi: "http://dx.doi.org/10.1109/CSF.2013.8" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csfw/MontaguPP13" researchr: "https://researchr.org/publication/MontaguPP13" cites: 0 citedby: 0 pages: "3-17" booktitle: "2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, LA, USA, June 26-28, 2013" publisher: "IEEE" isbn: "978-0-7695-5031-2" kind: "inproceedings" key: "MontaguPP13" - title: "A Record Calculus Based on Symmetric Concatenation" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1991" tags: - "rule-based" - "C++" researchr: "https://researchr.org/publication/HarperP91%3A0" cites: 0 citedby: 0 pages: "131-142" booktitle: "POPL" kind: "inproceedings" key: "HarperP91:0" - title: "Union Types for Semistructured Data" author: - name: "Peter Buneman" link: "https://researchr.org/alias/peter-buneman" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1999" doi: "http://link.springer.de/link/service/series/0558/bibs/1949/19490184.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1949/19490184.htm" tags: - "data-flow" - "C++" researchr: "https://researchr.org/publication/BunemanP99" cites: 0 citedby: 0 pages: "184-207" booktitle: "Research Issues in Structured and Semistructured Database Programming, 7th International Workshop on Database Programming Languages, DBPL 99, Kinloch Rannoch, Scotland, UK, September 1-3, 1999, Revised Papers" editor: - name: "Richard C. H. Connor" link: "https://researchr.org/alias/richard-c.-h.-connor" - name: "Alberto O. Mendelzon" link: "https://researchr.org/alias/alberto-o.-mendelzon" volume: "1949" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-41481-9" kind: "inproceedings" key: "BunemanP99" - title: "Types and programming languages" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2002" links: dblp: "http://dblp.uni-trier.de/rec/bibtex/books/daglib/0005958" tags: - "programming languages" - "C++" - "programming" researchr: "https://researchr.org/publication/0005958" cites: 0 citedby: 0 publisher: "MIT Press" isbn: "978-0-262-16209-8" kind: "book" key: "0005958" - title: "XML Goes Native: Run-Time Representations for Xtatic" author: - name: "Vladimir Gapeyev" link: "https://researchr.org/alias/vladimir-gapeyev" - name: "Michael Y. Levin" link: "https://researchr.org/alias/michael-y.-levin" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Alan Schmitt" link: "https://researchr.org/alias/alan-schmitt" year: "2005" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3443&spage=43" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3443&spage=43" tags: - "XML" - "XML Schema" - "C++" researchr: "https://researchr.org/publication/GapeyevLPS05" cites: 0 citedby: 0 pages: "43-58" booktitle: "Compiler Construction, 14th International Conference, CC 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings" editor: - name: "Rastislav Bodík" link: "https://researchr.org/alias/rastislav-bod%C3%ADk" volume: "3443" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-25411-0" kind: "inproceedings" key: "GapeyevLPS05" - title: "Local Type Inference" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "David N. Turner" link: "https://researchr.org/alias/david-n.-turner" year: "1998" doi: "http://doi.acm.org/10.1145/268946.268967" links: doi: "http://doi.acm.org/10.1145/268946.268967" successor: "https://researchr.org/publication/PierceT-TOPLAS-2000" tags: - "type inference" - "C++" - "local type inference" researchr: "https://researchr.org/publication/PierceT98" cites: 0 citedby: 0 pages: "252-265" booktitle: "Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages" address: "New York, NY, USA" publisher: "ACM" kind: "inproceedings" key: "PierceT98" - title: "Beginner's luck: a language for property-based generators" author: - name: "Leonidas Lampropoulos" link: "https://researchr.org/alias/leonidas-lampropoulos" - name: "Diane Gallois-Wong" link: "https://researchr.org/alias/diane-gallois-wong" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "John Hughes" link: "http://www.cse.chalmers.se/~rjmh" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Li-yao Xia" link: "https://researchr.org/alias/li-yao-xia" year: "2017" doi: "http://dl.acm.org/citation.cfm?id=3009868" links: doi: "http://dl.acm.org/citation.cfm?id=3009868" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/LampropoulosGHH17" researchr: "https://researchr.org/publication/LampropoulosGHH17" cites: 0 citedby: 0 pages: "114-129" booktitle: "Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017" editor: - name: "Giuseppe Castagna" link: "https://researchr.org/alias/giuseppe-castagna" - name: "Andrew D. Gordon" link: "https://researchr.org/alias/andrew-d.-gordon" publisher: "ACM" isbn: "978-1-4503-4660-3" kind: "inproceedings" key: "LampropoulosGHH17" - title: "A bisimulation for dynamic sealing" author: - name: "Eijiro Sumii" link: "https://researchr.org/alias/eijiro-sumii" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2004" doi: "http://doi.acm.org/10.1145/964001.964015" links: doi: "http://doi.acm.org/10.1145/964001.964015" tags: - "C++" researchr: "https://researchr.org/publication/SumiiP04" cites: 0 citedby: 0 pages: "161-172" booktitle: "Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004" editor: - name: "Neil D. Jones" link: "http://www.diku.dk/hjemmesider/ansatte/neil/" - name: "Xavier Leroy" link: "http://pauillac.inria.fr/~xleroy/" publisher: "ACM" isbn: "1-58113-729-X" kind: "inproceedings" key: "SumiiP04" - title: "Programming Language Foundations" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Chris Casinghino" link: "https://researchr.org/alias/chris-casinghino" - name: "Marco Gaboardi" link: "https://researchr.org/alias/marco-gaboardi" - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Vilhelm Sjöberg" link: "https://researchr.org/alias/vilhelm-sj%C3%B6berg" - name: "Andrew Tolmach" link: "https://researchr.org/alias/andrew-tolmach" - name: " Brent Yorgey" link: "https://researchr.org/alias/brent-yorgey" year: "2018" month: "May" note: "Version 5.5. \\url{http://www.cis.upenn.edu/~bcpierce/sf}" researchr: "https://researchr.org/publication/PierceSF2" cites: 0 citedby: 0 series: "Software Foundations series, volume 2" address: "Philadelphia, USA" publisher: "Electronic textbook" kind: "book" key: "PierceSF2" - title: "Verification challenges of pervasive information flow" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2012" doi: "http://doi.acm.org/10.1145/2103776.2103778" links: doi: "http://doi.acm.org/10.1145/2103776.2103778" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/plpv/Pierce12" researchr: "https://researchr.org/publication/Pierce12-0" cites: 0 citedby: 0 pages: "1-2" booktitle: "Proceedings of the sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012" editor: - name: "Koen Claessen" link: "http://www.cse.chalmers.se/~koen/" - name: "Nikhil Swamy" link: "https://researchr.org/alias/nikhil-swamy" publisher: "ACM" isbn: "978-1-4503-1125-0" kind: "inproceedings" key: "Pierce12-0" - title: "Bounded Existentials and Minimal Typing" author: - name: "Giorgio Ghelli" link: "https://researchr.org/alias/giorgio-ghelli" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1998" doi: "http://dx.doi.org/10.1016/S0304-3975(96)00300-3" links: doi: "http://dx.doi.org/10.1016/S0304-3975(96)00300-3" tags: - "C++" researchr: "https://researchr.org/publication/GhelliP98" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "193" number: "1-2" pages: "75-96" kind: "article" key: "GhelliP98" - title: "Higher-Order Intersection Types and Multiple Inheritance" author: - name: "Adriana B. Compagnoni" link: "https://researchr.org/alias/adriana-b.-compagnoni" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1996" tags: - "C++" researchr: "https://researchr.org/publication/CompagnoniP96" cites: 0 citedby: 0 journal: "Mathematical Structures in Computer Science" volume: "6" number: "5" pages: "469-501" kind: "article" key: "CompagnoniP96" - title: "Basic category theory for computer scientists" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1991" links: dblp: "http://dblp.uni-trier.de/rec/bibtex/books/daglib/0069193" tags: - "C++" researchr: "https://researchr.org/publication/0069193" cites: 0 citedby: 0 series: "Foundations of computing" publisher: "MIT Press" isbn: "978-0-262-66071-6" kind: "book" key: "0069193" - title: "Dynamic Typing in a Statically-Typed Language" author: - name: "Martín Abadi" link: "http://users.soe.ucsc.edu/~abadi/home.html" - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Gordon D. Plotkin" link: "https://researchr.org/alias/gordon-d.-plotkin" year: "1989" tags: - "C++" researchr: "https://researchr.org/publication/AbadiCPP89" cites: 0 citedby: 0 pages: "213-227" booktitle: "POPL" kind: "inproceedings" key: "AbadiCPP89" - title: "Architectural Support for Software-Defined Metadata Processing" author: - name: "Udit Dhawan" link: "https://researchr.org/alias/udit-dhawan" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Raphael Rubin" link: "https://researchr.org/alias/raphael-rubin" - name: "Nikos Vasilakis" link: "https://researchr.org/alias/nikos-vasilakis" - name: "Silviu Chiricescu" link: "https://researchr.org/alias/silviu-chiricescu" - name: "Jonathan M. Smith" link: "https://researchr.org/alias/jonathan-m.-smith" - name: "Thomas F. Knight Jr." link: "https://researchr.org/alias/thomas-f.-knight-jr." - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "André DeHon" link: "https://researchr.org/alias/andr%C3%A9-dehon" year: "2015" doi: "http://doi.acm.org/10.1145/2694344.2694383" links: doi: "http://doi.acm.org/10.1145/2694344.2694383" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/asplos/DhawanHRVCSKPD15" researchr: "https://researchr.org/publication/DhawanHRVCSKPD15" cites: 0 citedby: 0 pages: "487-502" booktitle: "Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '15, Istanbul, Turkey, March 14-18, 2015" editor: - name: "Özcan Özturk" link: "https://researchr.org/alias/%C3%B6zcan-%C3%B6zturk" - name: "Kemal Ebcioglu" link: "https://researchr.org/alias/kemal-ebcioglu" - name: "Sandhya Dwarkadas" link: "https://researchr.org/alias/sandhya-dwarkadas" publisher: "ACM" isbn: "978-1-4503-2835-7" kind: "inproceedings" key: "DhawanHRVCSKPD15" - title: "Behavioral Equivalence in the Polymorphic Pi-calculus" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Davide Sangiorgi" link: "https://researchr.org/alias/davide-sangiorgi" year: "1997" doi: "http://doi.acm.org/10.1145/263699.263729" links: doi: "http://doi.acm.org/10.1145/263699.263729" tags: - "C++" researchr: "https://researchr.org/publication/PierceS97%3A0" cites: 0 citedby: 0 pages: "242-255" booktitle: "Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages" kind: "inproceedings" key: "PierceS97:0" - title: "Combinators for bi-directional tree transformations: a linguistic approach to the view update problem" author: - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Michael B. Greenwald" link: "https://researchr.org/alias/michael-b.-greenwald" - name: "Jonathan T. Moore" link: "https://researchr.org/alias/jonathan-t.-moore" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Alan Schmitt" link: "https://researchr.org/alias/alan-schmitt" year: "2005" doi: "http://doi.acm.org/10.1145/1040305.1040325" links: doi: "http://doi.acm.org/10.1145/1040305.1040325" tags: - "C++" - "systematic-approach" - "transformation" researchr: "https://researchr.org/publication/FosterGMPS05" cites: 0 citedby: 0 pages: "233-246" booktitle: "Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005" editor: - name: "Jens Palsberg" link: "https://researchr.org/alias/jens-palsberg" - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" publisher: "ACM" isbn: "1-58113-830-X" kind: "inproceedings" key: "FosterGMPS05" - title: "Programming language techniques for differential privacy" author: - name: "Gilles Barthe" link: "https://researchr.org/alias/gilles-barthe" - name: "Marco Gaboardi" link: "https://researchr.org/alias/marco-gaboardi" - name: "Justin Hsu" link: "https://researchr.org/alias/justin-hsu" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2016" doi: "http://doi.acm.org/10.1145/2893582.2893591" links: doi: "http://doi.acm.org/10.1145/2893582.2893591" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/siglog/BartheGHP16" researchr: "https://researchr.org/publication/BartheGHP16" cites: 0 citedby: 0 journal: "SIGLOG News" volume: "3" number: "1" pages: "34-53" kind: "article" key: "BartheGHP16" - title: "Decidable Bounded Quantification" author: - name: "Giuseppe Castagna" link: "https://researchr.org/alias/giuseppe-castagna" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1994" tags: - "C++" researchr: "https://researchr.org/publication/CastagnaP94" cites: 0 citedby: 0 pages: "151-162" booktitle: "Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages" kind: "inproceedings" key: "CastagnaP94" - title: "A bisimulation for type abstraction and recursion" author: - name: "Eijiro Sumii" link: "https://researchr.org/alias/eijiro-sumii" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2005" doi: "http://doi.acm.org/10.1145/1040305.1040311" links: doi: "http://doi.acm.org/10.1145/1040305.1040311" tags: - "C++" - "abstraction" researchr: "https://researchr.org/publication/SumiiP05" cites: 0 citedby: 0 pages: "63-74" booktitle: "Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005" editor: - name: "Jens Palsberg" link: "https://researchr.org/alias/jens-palsberg" - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" publisher: "ACM" isbn: "1-58113-830-X" kind: "inproceedings" key: "SumiiP05" - title: "On Binary Methods" author: - name: "Kim B. Bruce" link: "https://researchr.org/alias/kim-b.-bruce" - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Giuseppe Castagna" link: "https://researchr.org/alias/giuseppe-castagna" - name: "Jonathan Eifrig" link: "https://researchr.org/alias/jonathan-eifrig" - name: "Scott F. Smith" link: "https://researchr.org/alias/scott-f.-smith" - name: "Valery Trifonov" link: "https://researchr.org/alias/valery-trifonov" - name: "Gary T. Leavens" link: "https://researchr.org/alias/gary-t.-leavens" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1995" tags: - "C++" researchr: "https://researchr.org/publication/BruceCCESTLP95" cites: 0 citedby: 0 journal: "TAPOS" volume: "1" number: "3" pages: "221-242" kind: "article" key: "BruceCCESTLP95" - title: "Differential Privacy: An Economic Method for Choosing Epsilon" author: - name: "Justin Hsu" link: "https://researchr.org/alias/justin-hsu" - name: "Marco Gaboardi" link: "https://researchr.org/alias/marco-gaboardi" - name: "Andreas Haeberlen" link: "https://researchr.org/alias/andreas-haeberlen" - name: "Sanjeev Khanna" link: "https://researchr.org/alias/sanjeev-khanna" - name: "Arjun Narayan" link: "https://researchr.org/alias/arjun-narayan" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Aaron Roth" link: "https://researchr.org/alias/aaron-roth" year: "2014" doi: "http://dx.doi.org/10.1109/CSF.2014.35" links: doi: "http://dx.doi.org/10.1109/CSF.2014.35" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csfw/HsuGHKNPR14" researchr: "https://researchr.org/publication/HsuGHKNPR14" cites: 0 citedby: 0 pages: "398-410" booktitle: "IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014" publisher: "IEEE" kind: "inproceedings" key: "HsuGHKNPR14" - title: "Linear dependent types for differential privacy" author: - name: "Marco Gaboardi" link: "https://researchr.org/alias/marco-gaboardi" - name: "Andreas Haeberlen" link: "https://researchr.org/alias/andreas-haeberlen" - name: "Justin Hsu" link: "https://researchr.org/alias/justin-hsu" - name: "Arjun Narayan" link: "https://researchr.org/alias/arjun-narayan" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2013" doi: "http://doi.acm.org/10.1145/2429069.2429113" links: doi: "http://doi.acm.org/10.1145/2429069.2429113" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/GaboardiHHNP13" researchr: "https://researchr.org/publication/GaboardiHHNP13" cites: 0 citedby: 0 pages: "357-370" booktitle: "The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013" editor: - name: "Roberto Giacobazzi" link: "https://researchr.org/alias/roberto-giacobazzi" - name: "Radhia Cousot" link: "https://researchr.org/alias/radhia-cousot" publisher: "ACM" isbn: "978-1-4503-1832-7" kind: "inproceedings" key: "GaboardiHHNP13" - title: "Comparing Object Encodings" author: - name: "Kim B. Bruce" link: "https://researchr.org/alias/kim-b.-bruce" - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1999" tags: - "meta-model" - "C++" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/BruceCP99" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "155" number: "1-2" pages: "108-133" kind: "article" key: "BruceCP99" - title: "Preface" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" year: "2012" doi: "http://dx.doi.org/10.1007/s10817-012-9254-5" links: doi: "http://dx.doi.org/10.1007/s10817-012-9254-5" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jar/PierceW12" researchr: "https://researchr.org/publication/PierceW12" cites: 0 citedby: 0 journal: "Journal of Automated Reasoning" volume: "49" number: "3" pages: "301-302" kind: "article" key: "PierceW12" - title: "Lambda, the ultimate TA: using a proof assistant to teach programming language foundations" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2009" doi: "http://doi.acm.org/10.1145/1596550.1596552" links: doi: "http://doi.acm.org/10.1145/1596550.1596552" tags: - "programming languages" - "proof assistant" - "C++" - "programming" researchr: "https://researchr.org/publication/Pierce09-1" cites: 0 citedby: 0 pages: "121-122" booktitle: "Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009" editor: - name: "Graham Hutton" link: "https://researchr.org/alias/graham-hutton" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" publisher: "ACM" isbn: "978-1-60558-332-7" kind: "inproceedings" key: "Pierce09-1" - title: "Mysteries of DropBox: Property-Based Testing of a Distributed Synchronization Service" author: - name: "John Hughes" link: "http://www.cse.chalmers.se/~rjmh" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Thomas Arts" link: "https://researchr.org/alias/thomas-arts" - name: "Ulf Norell" link: "https://researchr.org/alias/ulf-norell" year: "2016" doi: "http://doi.ieeecomputersociety.org/10.1109/ICST.2016.37" links: doi: "http://doi.ieeecomputersociety.org/10.1109/ICST.2016.37" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icst/HughesPAN16" researchr: "https://researchr.org/publication/HughesPAN16" cites: 0 citedby: 0 pages: "135-145" booktitle: "2016 IEEE International Conference on Software Testing, Verification and Validation, ICST 2016, Chicago, IL, USA, April 11-15, 2016" publisher: "IEEE Computer Society" isbn: "978-1-5090-1827-7" kind: "inproceedings" key: "HughesPAN16" - title: "Distance makes the types grow stronger: a calculus for differential privacy" author: - name: "Jason Reed" link: "https://researchr.org/alias/jason-reed" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2010" doi: "http://doi.acm.org/10.1145/1863543.1863568" links: doi: "http://doi.acm.org/10.1145/1863543.1863568" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/ReedP10" tags: - "C++" researchr: "https://researchr.org/publication/ReedP10" cites: 0 citedby: 0 pages: "157-168" booktitle: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010" editor: - name: "Paul Hudak" link: "https://researchr.org/alias/paul-hudak" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-794-3" kind: "inproceedings" key: "ReedP10" - title: "The Weird World of Bi-directional Programming" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2006" doi: "http://dx.doi.org/10.1007/11693024_23" links: doi: "http://dx.doi.org/10.1007/11693024_23" tags: - "C++" - "programming" researchr: "https://researchr.org/publication/Pierce06" cites: 0 citedby: 0 pages: "342" booktitle: "Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings" editor: - name: "Peter Sestoft" link: "https://researchr.org/alias/peter-sestoft" volume: "3924" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-33095-X" kind: "inproceedings" key: "Pierce06" - title: "Object-Oriented Programming without Recursive Types" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "David N. Turner" link: "https://researchr.org/alias/david-n.-turner" year: "1993" tags: - "object-oriented programming" - "meta programming" - "C++" - "programming" - "subject-oriented programming" - "Meta-Environment" - "feature-oriented programming" - "meta-objects" researchr: "https://researchr.org/publication/PierceT93" cites: 0 citedby: 0 pages: "299-312" booktitle: "Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages" kind: "inproceedings" key: "PierceT93" - title: "A verified information-flow architecture" author: - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Nathan Collins" link: "https://researchr.org/alias/nathan-collins" - name: "André DeHon" link: "https://researchr.org/alias/andr%C3%A9-dehon" - name: "Delphine Demange" link: "https://researchr.org/alias/delphine-demange" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "David Pichardie" link: "https://researchr.org/alias/david-pichardie" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Randy Pollack" link: "https://researchr.org/alias/randy-pollack" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" year: "2014" doi: "http://doi.acm.org/10.1145/2535838.2535839" links: doi: "http://doi.acm.org/10.1145/2535838.2535839" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/AmorimCDDHPPPT14" researchr: "https://researchr.org/publication/AmorimCDDHPPPT14" cites: 0 citedby: 0 pages: "165-178" booktitle: "The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014" editor: - name: "Suresh Jagannathan" link: "https://researchr.org/alias/suresh-jagannathan" - name: "Peter Sewell" link: "https://researchr.org/alias/peter-sewell" publisher: "ACM" isbn: "978-1-4503-2544-8" kind: "inproceedings" key: "AmorimCDDHPPPT14" - title: "Unison: A File Synchronizer and Its Specification" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Jérôme Vouillon" link: "https://researchr.org/alias/j%C3%A9r%C3%B4me-vouillon" year: "2001" doi: "http://link.springer.de/link/service/series/0558/bibs/2215/22150560.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2215/22150560.htm" tags: - "synchronization" - "C++" researchr: "https://researchr.org/publication/PierceV01" cites: 0 citedby: 0 pages: "560" booktitle: "Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings" editor: - name: "Naoki Kobayashi" link: "https://researchr.org/alias/naoki-kobayashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" volume: "2215" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-42736-8" kind: "inproceedings" key: "PierceV01" - title: "Explicit Secrecy: A Policy for Taint Tracking" author: - name: "Daniel Schoepe" link: "https://researchr.org/alias/daniel-schoepe" - name: "Musard Balliu" link: "https://researchr.org/alias/musard-balliu" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Andrei Sabelfeld" link: "https://researchr.org/alias/andrei-sabelfeld" year: "2016" doi: "http://dx.doi.org/10.1109/EuroSP.2016.14" links: doi: "http://dx.doi.org/10.1109/EuroSP.2016.14" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/eurosp/SchoepeBPS16" researchr: "https://researchr.org/publication/SchoepeBPS16" cites: 0 citedby: 0 pages: "15-30" booktitle: "IEEE European Symposium on Security and Privacy, EuroS&P 2016, Saarbrücken, Germany, March 21-24, 2016" publisher: "IEEE" isbn: "978-1-5090-1752-2" kind: "inproceedings" key: "SchoepeBPS16" - title: "Generating good generators for inductive relations" author: - name: "Leonidas Lampropoulos" link: "https://researchr.org/alias/leonidas-lampropoulos" - name: "Zoe Paraskevopoulou" link: "https://researchr.org/alias/zoe-paraskevopoulou" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2018" doi: "http://doi.acm.org/10.1145/3158133" links: doi: "http://doi.acm.org/10.1145/3158133" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/LampropoulosPP18" researchr: "https://researchr.org/publication/LampropoulosPP18" cites: 0 citedby: 0 journal: "Proceedings of the ACM on Programming Languages" volume: "2" number: "POPL" kind: "article" key: "LampropoulosPP18" - title: "Types and Programming Languages: The Next Generation" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2003" doi: "http://csdl.computer.org/comp/proceedings/lics/2003/1884/00/18840032abs.htm" links: doi: "http://csdl.computer.org/comp/proceedings/lics/2003/1884/00/18840032abs.htm" tags: - "programming languages" - "C++" - "programming" researchr: "https://researchr.org/publication/Pierce03%3A3" cites: 0 citedby: 0 pages: "32" booktitle: "18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings" publisher: "IEEE Computer Society" isbn: "0-7695-1884-2" kind: "inproceedings" key: "Pierce03:3" - title: "Advanced module systems: a guide for the perplexed (abstract of invited talk)" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2000" doi: "http://doi.acm.org/10.1145/351240.351252" links: doi: "http://doi.acm.org/10.1145/351240.351252" tags: - "C++" researchr: "https://researchr.org/publication/HarperP00" cites: 0 citedby: 0 pages: "130" booktitle: "ICFP" kind: "inproceedings" key: "HarperP00" - title: "Bounded Quantification is Undecidable" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1992" tags: - "C++" researchr: "https://researchr.org/publication/Pierce92%3A0" cites: 0 citedby: 0 pages: "305-315" booktitle: "POPL" kind: "inproceedings" key: "Pierce92:0" - title: "TinkerType: a language for playing with formal systems" author: - name: "Michael Y. Levin" link: "https://researchr.org/alias/michael-y.-levin" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2003" doi: "http://dx.doi.org/10.1017/S0956796802004550" abstract: "TinkerType is a pragmatic framework for compact and modular description of formal systems (type systems, operational semantics, logics, etc.). A family of related systems is broken down into a set of clauses – individual inference rules – and a set of features controlling the inclusion of clauses in particular systems. Simple static checks are used to help maintain consistency of the generated systems. We present TinkerType and its implementation and describe its application to two substantial repositories of typed lambda-calculi. The first repository covers a broad range of typing features, including subtyping, polymorphism, type operators and kinding, computational effects, and dependent types. It describes both declarative and algorithmic aspects of the systems, and can be used with our tool, the TinkerType Assembler, to generate calculi either in the form of typeset collections of inference rules or as executable ML typecheckers. The second repository addresses a smaller collection of systems, and provides modularized proofs of basic safety properties." links: doi: "http://dx.doi.org/10.1017/S0956796802004550" tags: - "control systems" - "semantics" - "type inference" - "rule-based" - "application framework" - "formal semantics" - "type system" - "rules" - "C++" - "subtyping" - "type checking" - "consistency" - "operational semantics" - "logic" researchr: "https://researchr.org/publication/LevinP03" cites: 31 citedby: 0 journal: "Journal of Functional Programming" volume: "13" number: "2" pages: "295-316" kind: "article" key: "LevinP03" - title: "Polymorphic Contracts" author: - name: "João Filipe Belo" link: "https://researchr.org/alias/jo%C3%A3o-filipe-belo" - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: "Atsushi Igarashi" link: "https://researchr.org/alias/atsushi-igarashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2011" doi: "http://dx.doi.org/10.1007/978-3-642-19718-5_2" links: doi: "http://dx.doi.org/10.1007/978-3-642-19718-5_2" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/BeloGIP11" tags: - "contracts" - "C++" researchr: "https://researchr.org/publication/BeloGIP11" cites: 0 citedby: 0 pages: "18-37" booktitle: "Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings" editor: - name: "Gilles Barthe" link: "https://researchr.org/alias/gilles-barthe" volume: "6602" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-19717-8" kind: "inproceedings" key: "BeloGIP11" - title: "Dynamic Typing in Polymorphic Languages" author: - name: "Martín Abadi" link: "http://users.soe.ucsc.edu/~abadi/home.html" - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Didier Rémy" link: "https://researchr.org/alias/didier-r%C3%A9my" year: "1995" tags: - "C++" researchr: "https://researchr.org/publication/AbadiCPR95" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "5" number: "1" pages: "111-130" kind: "article" key: "AbadiCPR95" - title: "Updatable Security Views" author: - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Steve Zdancewic" link: "https://researchr.org/alias/steve-zdancewic" year: "2009" doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2009.25" links: doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2009.25" tags: - "C++" - "security" researchr: "https://researchr.org/publication/FosterPZ09" cites: 0 citedby: 0 pages: "60-74" booktitle: "Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8-10, 2009" publisher: "IEEE Computer Society" isbn: "978-0-7695-3712-2" kind: "inproceedings" key: "FosterPZ09" - title: "Regular expression types for XML" author: - name: "Haruo Hosoya" link: "https://researchr.org/alias/haruo-hosoya" - name: "Jerome Vouillon" link: "https://researchr.org/alias/jerome-vouillon" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2000" doi: "http://doi.acm.org/10.1145/351240.351242" links: doi: "http://doi.acm.org/10.1145/351240.351242" tags: - "XML" - "XML Schema" - "C++" researchr: "https://researchr.org/publication/HosoyaVP00" cites: 0 citedby: 1 pages: "11-22" booktitle: "ICFP" kind: "inproceedings" key: "HosoyaVP00" - title: "A verified information-flow architecture" author: - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Nathan Collins" link: "https://researchr.org/alias/nathan-collins" - name: "André DeHon" link: "https://researchr.org/alias/andr%C3%A9-dehon" - name: "Delphine Demange" link: "https://researchr.org/alias/delphine-demange" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "David Pichardie" link: "https://researchr.org/alias/david-pichardie" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Randy Pollack" link: "https://researchr.org/alias/randy-pollack" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" year: "2016" doi: "http://dx.doi.org/10.3233/JCS-15784" links: doi: "http://dx.doi.org/10.3233/JCS-15784" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jcs/AmorimCDDHPPPT16" researchr: "https://researchr.org/publication/AmorimCDDHPPPT16" cites: 0 citedby: 0 journal: "Journal of Computer Security" volume: "24" number: "6" pages: "689-734" kind: "article" key: "AmorimCDDHPPPT16" - title: "Differential Privacy Under Fire" author: - name: "Andreas Haeberlen" link: "https://researchr.org/alias/andreas-haeberlen" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Arjun Narayan" link: "https://researchr.org/alias/arjun-narayan" year: "2011" doi: "http://static.usenix.org/events/sec11/tech/full_papers/Haeberlen.pdf" links: doi: "http://static.usenix.org/events/sec11/tech/full_papers/Haeberlen.pdf" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/uss/HaeberlenPN11" researchr: "https://researchr.org/publication/HaeberlenPN11" cites: 0 citedby: 0 booktitle: "20th USENIX Security Symposium, San Francisco, CA, USA, August 8-12, 2011, Proceedings" publisher: "USENIX Association" kind: "inproceedings" key: "HaeberlenPN11" - title: "The Meaning of Memory Safety" author: - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2018" doi: "https://doi.org/10.1007/978-3-319-89722-6_4" links: doi: "https://doi.org/10.1007/978-3-319-89722-6_4" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/post/AmorimHP18" researchr: "https://researchr.org/publication/AmorimHP18" cites: 0 citedby: 0 pages: "79-105" booktitle: "Principles of Security and Trust - 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings" editor: - name: "Lujo Bauer" link: "https://researchr.org/alias/lujo-bauer" - name: "Ralf Küsters" link: "https://researchr.org/alias/ralf-k%C3%BCsters" volume: "10804" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-89722-6" kind: "inproceedings" key: "AmorimHP18" - title: "Type Systems for Concurrent Calculi (Abstract)" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1998" doi: "http://link.springer.de/link/service/series/0558/bibs/1466/14660364.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1466/14660364.htm" tags: - "type system" - "C++" researchr: "https://researchr.org/publication/Pierce98" cites: 0 citedby: 0 pages: "364-365" booktitle: "CONCUR 98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings" editor: - name: "Davide Sangiorgi" link: "https://researchr.org/alias/davide-sangiorgi" - name: "Robert de Simone" link: "https://researchr.org/alias/robert-de-simone" volume: "1466" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-64896-8" kind: "inproceedings" key: "Pierce98" - title: "Relational lenses: a language for updatable views" author: - name: "Aaron Bohannon" link: "https://researchr.org/alias/aaron-bohannon" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Jeffrey A. Vaughan" link: "https://researchr.org/alias/jeffrey-a.-vaughan" year: "2006" doi: "http://doi.acm.org/10.1145/1142351.1142399" links: doi: "http://doi.acm.org/10.1145/1142351.1142399" tags: - "C++" - "lenses" researchr: "https://researchr.org/publication/BohannonPV06" cites: 0 citedby: 0 pages: "338-347" booktitle: "Proceedings of the Twenty-Fifth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 26-28, 2006, Chicago, Illinois, USA" editor: - name: "Stijn Vansummeren" link: "https://researchr.org/alias/stijn-vansummeren" publisher: "ACM" isbn: "1-59593-318-2" kind: "inproceedings" key: "BohannonPV06" - title: "XDuce: A Typed XML Processing Language (Preliminary Report)" author: - name: "Haruo Hosoya" link: "https://researchr.org/alias/haruo-hosoya" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2000" doi: "http://link.springer.de/link/service/series/0558/bibs/1997/19970226.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1997/19970226.htm" tags: - "XML" - "XML Schema" - "C++" researchr: "https://researchr.org/publication/HosoyaP00a" cites: 0 citedby: 0 pages: "226-244" booktitle: "The World Wide Web and Databases, Third International Workshop WebDB 2000, Dallas, Texas, USA, Maaay 18-19, 2000, Selected Papers" editor: - name: "Dan Suciu" link: "https://researchr.org/alias/dan-suciu" - name: "Gottfried Vossen" link: "https://researchr.org/alias/gottfried-vossen" volume: "1997" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-41826-1" kind: "inproceedings" key: "HosoyaP00a" - title: "Behavioral equivalence in the polymorphic pi-calculus" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Davide Sangiorgi" link: "https://researchr.org/alias/davide-sangiorgi" year: "2000" doi: "http://doi.acm.org/10.1145/337244.337261" links: doi: "http://doi.acm.org/10.1145/337244.337261" tags: - "C++" researchr: "https://researchr.org/publication/PierceS00" cites: 0 citedby: 0 journal: "Journal of the ACM" volume: "47" number: "3" pages: "531-584" kind: "article" key: "PierceS00" - title: "Editorial - Third Workshop on Foundations of Object-Oriented Languages" author: - name: "Kim B. Bruce" link: "https://researchr.org/alias/kim-b.-bruce" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1998" tags: - "meta-model" - "C++" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/BruceP98" cites: 0 citedby: 0 journal: "TAPOS" volume: "4" number: "1" pages: "1" kind: "article" key: "BruceP98" - title: "Information and Computation special issue from TACS 2001" author: - name: "Naoki Kobayashi" link: "https://researchr.org/alias/naoki-kobayashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2003" doi: "http://dx.doi.org/10.1016/S0890-5401(03)00173-1" links: doi: "http://dx.doi.org/10.1016/S0890-5401(03)00173-1" tags: - "C++" researchr: "https://researchr.org/publication/KobayashiP03" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "186" number: "2" pages: "163-164" kind: "article" key: "KobayashiP03" - title: "Logical Relations for Encryption" author: - name: "Eijiro Sumii" link: "https://researchr.org/alias/eijiro-sumii" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2003" tags: - "C++" researchr: "https://researchr.org/publication/SumiiP03" cites: 0 citedby: 0 journal: "Journal of Computer Security" volume: "11" number: "4" pages: "521-554" kind: "article" key: "SumiiP03" - title: "Regular expression pattern matching for XML" author: - name: "Haruo Hosoya" link: "https://researchr.org/alias/haruo-hosoya" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2001" doi: "http://doi.acm.org/10.1145/360204.360209" links: doi: "http://doi.acm.org/10.1145/360204.360209" tags: - "XML" - "XML Schema" - "C++" - "pattern matching" researchr: "https://researchr.org/publication/HosoyaP01" cites: 0 citedby: 0 pages: "67-80" booktitle: "Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages" series: "POPL" publisher: "Association for Computing Machinery" kind: "inproceedings" key: "HosoyaP01" - title: "It Is Time to Mechanize Programming Language Metatheory" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Peter Sewell" link: "https://researchr.org/alias/peter-sewell" - name: "Stephanie Weirich" link: "http://www.cis.upenn.edu/~sweirich/" - name: "Steve Zdancewic" link: "https://researchr.org/alias/steve-zdancewic" year: "2005" doi: "http://dx.doi.org/10.1007/978-3-540-69149-5_3" abstract: "How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researchers alike? One crucial step towards achieving these goals is mechanized reasoning about language metatheory. The time has come to bring together the theorem proving and programming language communities to address this problem. We have proposed the POPLMark challenge as a concrete set of benchmarks intended both for measuring progress in this area and for stimulating discussion and collaboration. Our goal is to push the boundaries of existing technology to the point where we can achieve mechanized metatheory for the masses. " links: doi: "http://dx.doi.org/10.1007/978-3-540-69149-5_3" tags: - "programming languages" - "program verification" - "C++" - "metatheory" - "programming" researchr: "https://researchr.org/publication/PierceSWZ05" cites: 22 citedby: 0 pages: "26-30" booktitle: "Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions" editor: - name: "Bertrand Meyer" link: "http://se.ethz.ch/~meyer/" - name: "Jim Woodcock" link: "https://researchr.org/alias/jim-woodcock" volume: "4171" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-69147-1" kind: "inproceedings" key: "PierceSWZ05" - title: "Simple Type-Theoretic Foundations for Object-Oriented Programming" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "David N. Turner" link: "https://researchr.org/alias/david-n.-turner" year: "1994" tags: - "object-oriented programming" - "meta programming" - "C++" - "programming" - "subject-oriented programming" - "Meta-Environment" - "feature-oriented programming" - "meta-objects" researchr: "https://researchr.org/publication/PierceT94" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "4" number: "2" pages: "207-247" kind: "article" key: "PierceT94" - title: "What is a File Synchronizer?" author: - name: "Sundar Balasubramaniam" link: "https://researchr.org/alias/sundar-balasubramaniam" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1998" doi: "http://doi.acm.org/10.1145/288235.288261" links: doi: "http://doi.acm.org/10.1145/288235.288261" tags: - "synchronization" - "C++" researchr: "https://researchr.org/publication/BalasubramaniamP98" cites: 0 citedby: 0 pages: "98-108" booktitle: "MOBICOM" kind: "inproceedings" key: "BalasubramaniamP98" - title: "Sensitivity analysis using type-based constraints" author: - name: "Loris D'Antoni" link: "https://researchr.org/alias/loris-d%27antoni" - name: "Marco Gaboardi" link: "https://researchr.org/alias/marco-gaboardi" - name: "Emilio Jesús Gallego Arias" link: "https://researchr.org/alias/emilio-jes%C3%BAs-gallego-arias" - name: "Andreas Haeberlen" link: "https://researchr.org/alias/andreas-haeberlen" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2013" doi: "http://doi.acm.org/10.1145/2505351.2505353" links: doi: "http://doi.acm.org/10.1145/2505351.2505353" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/DAntoniGAHP13" researchr: "https://researchr.org/publication/DAntoniGAHP13" cites: 0 citedby: 0 pages: "43-50" booktitle: "Proceedings of the 1st annual workshop on Functional programming concepts in domain-specific languages, FPCDSL@ICFP 2013, Boston, Massachusetts, USA, September 22, 2013" editor: - name: "Richard Lazarus" link: "https://researchr.org/alias/richard-lazarus" - name: "Assaf J. Kfoury" link: "https://researchr.org/alias/assaf-j.-kfoury" - name: "Jacob Beal" link: "https://researchr.org/alias/jacob-beal" publisher: "ACM" isbn: "978-1-4503-2380-2" kind: "inproceedings" key: "DAntoniGAHP13" - title: "Special Issue Dedicated to ICFP 2011 Editorial" author: - name: "Kenichi Asai" link: "http://pllab.is.ocha.ac.jp/~asai/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2013" doi: "http://dx.doi.org/10.1017/S0956796813000129" links: doi: "http://dx.doi.org/10.1017/S0956796813000129" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/AsaiP13" researchr: "https://researchr.org/publication/AsaiP13" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "23" number: "4" pages: "355-356" kind: "article" key: "AsaiP13" - title: "Concurrent Objects in a Process Calculus" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1994" tags: - "meta-model" - "C++" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/Pierce94" cites: 0 citedby: 0 pages: "187-215" booktitle: "Theory and Practice of Parallel Programming, International Workshop TPPP 94, Sendai, Japan, November 7-9, 1994, Proceedings" editor: - name: "Takayasu Ito" link: "https://researchr.org/alias/takayasu-ito" - name: "Akinori Yonezawa" link: "https://researchr.org/alias/akinori-yonezawa" volume: "907" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-59172-9" kind: "inproceedings" key: "Pierce94" - title: "Positive Subtyping" author: - name: "Martin Hofmann" link: "https://researchr.org/alias/martin-hofmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1995" tags: - "C++" - "subtyping" researchr: "https://researchr.org/publication/HofmannP95%3A0" cites: 0 citedby: 0 pages: "186-197" booktitle: "POPL" kind: "inproceedings" key: "HofmannP95:0" - title: "Testing noninterference, quickly" author: - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Leonidas Lampropoulos" link: "https://researchr.org/alias/leonidas-lampropoulos" - name: "Antal Spector-Zabusky" link: "https://researchr.org/alias/antal-spector-zabusky" - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Maxime Dénès" link: "https://researchr.org/alias/maxime-d%C3%A9n%C3%A8s" - name: "John Hughes" link: "http://www.cse.chalmers.se/~rjmh" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Dimitrios Vytiniotis" link: "https://researchr.org/alias/dimitrios-vytiniotis" year: "2016" doi: "http://dx.doi.org/10.1017/S0956796816000058" links: doi: "http://dx.doi.org/10.1017/S0956796816000058" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/HritcuLSADHPV16" researchr: "https://researchr.org/publication/HritcuLSADHPV16" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "26" kind: "article" key: "HritcuLSADHPV16" - title: "Recursive subtyping revealed" author: - name: "Vladimir Gapeyev" link: "https://researchr.org/alias/vladimir-gapeyev" - name: "Michael Y. Levin" link: "https://researchr.org/alias/michael-y.-levin" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2002" doi: "http://dx.doi.org/10.1017/S0956796802004318" links: doi: "http://dx.doi.org/10.1017/S0956796802004318" tags: - "C++" - "subtyping" researchr: "https://researchr.org/publication/GapeyevLP02" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "12" number: "6" pages: "511-548" kind: "article" key: "GapeyevLP02" - title: "Decoding Choice Encodings" author: - name: "Uwe Nestmann" link: "https://researchr.org/alias/uwe-nestmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1996" tags: - "C++" researchr: "https://researchr.org/publication/NestmannP96" cites: 0 citedby: 0 pages: "179-194" booktitle: "CONCUR 96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings" editor: - name: "Ugo Montanari" link: "https://researchr.org/alias/ugo-montanari" - name: "Vladimiro Sassone" link: "http://www.ecs.soton.ac.uk/people/vs" volume: "1119" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-61604-7" kind: "inproceedings" key: "NestmannP96" - title: "A Formal Investigation of" author: - name: "Sanjeev Khanna" link: "https://researchr.org/alias/sanjeev-khanna" - name: "Keshav Kunal" link: "https://researchr.org/alias/keshav-kunal" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2007" doi: "http://dx.doi.org/10.1007/978-3-540-77050-3_40" links: doi: "http://dx.doi.org/10.1007/978-3-540-77050-3_40" tags: - "C++" researchr: "https://researchr.org/publication/KhannaKP07" cites: 0 citedby: 0 pages: "485-496" booktitle: "FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, New Delhi, India, December 12-14, 2007, Proceedings" editor: - name: "Vikraman Arvind" link: "https://researchr.org/alias/vikraman-arvind" - name: "Sanjiva Prasad" link: "https://researchr.org/alias/sanjiva-prasad" volume: "4855" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-77049-7" kind: "inproceedings" key: "KhannaKP07" - title: "Foundational Calculi for Programming Languages" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1997" tags: - "programming languages" - "C++" - "programming" researchr: "https://researchr.org/publication/Pierce97%3A0" cites: 0 citedby: 0 pages: "2190-2207" booktitle: "The Computer Science and Engineering Handbook" editor: - name: "Allen B. Tucker" link: "https://researchr.org/alias/allen-b.-tucker" publisher: "CRC Press" isbn: "0-8493-2909-4" kind: "incollection" key: "Pierce97:0" - title: "Logical Relations for Encryption" author: - name: "Eijiro Sumii" link: "https://researchr.org/alias/eijiro-sumii" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2001" doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2001.1" links: doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2001.1" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csfw/SumiiP01" researchr: "https://researchr.org/publication/SumiiP01" cites: 0 citedby: 0 pages: "256-269" booktitle: "14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada" publisher: "IEEE Computer Society" isbn: "0-7695-1146-5" kind: "inproceedings" key: "SumiiP01" - title: "A Unifying Type-Theoretic Framework for Objects" author: - name: "Martin Hofmann" link: "https://researchr.org/alias/martin-hofmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1994" tags: - "meta-model" - "C++" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/HofmannP94" cites: 0 citedby: 0 pages: "251-262" booktitle: "STACS 94, 11th Annual Symposium on Theoretical Aspects of Computer Science, Caen, France, February 24-26, 1994, Proceedings" editor: - name: "Patrice Enjalbert" link: "https://researchr.org/alias/patrice-enjalbert" - name: "Ernst W. Mayr" link: "https://researchr.org/alias/ernst-w.-mayr" - name: "Klaus W. Wagner" link: "https://researchr.org/alias/klaus-w.-wagner" volume: "775" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-57785-8" kind: "inproceedings" key: "HofmannP94" - title: "The science of deep specification (keynote)" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2016" doi: "http://doi.acm.org/10.1145/2984043.2998388" links: doi: "http://doi.acm.org/10.1145/2984043.2998388" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/oopsla/Pierce16" researchr: "https://researchr.org/publication/Pierce16-0" cites: 0 citedby: 0 pages: "1" booktitle: "Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, SPLASH 2016, Amsterdam, Netherlands, October 30 - November 4, 2016" editor: - name: "Eelco Visser" link: "http://eelcovisser.org" publisher: "ACM" isbn: "978-1-4503-4437-1" kind: "inproceedings" key: "Pierce16-0" - title: "Differential privacy for collaborative security" author: - name: "Jason Reed" link: "https://researchr.org/alias/jason-reed" - name: "Adam J. Aviv" link: "https://researchr.org/alias/adam-j.-aviv" - name: "Daniel Wagner" link: "https://researchr.org/alias/daniel-wagner" - name: "Andreas Haeberlen" link: "https://researchr.org/alias/andreas-haeberlen" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Jonathan M. Smith" link: "https://researchr.org/alias/jonathan-m.-smith" year: "2010" doi: "http://doi.acm.org/10.1145/1752046.1752047" links: doi: "http://doi.acm.org/10.1145/1752046.1752047" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/eurosec/ReedAWHPS10" tags: - "C++" - "security" researchr: "https://researchr.org/publication/ReedAWHPS10" cites: 0 citedby: 0 pages: "1-7" booktitle: "Proceedings of the Third European Workshop on System Security, EUROSEC 2010, Paris, France, April 13, 2010" editor: - name: "Manuel Costa" link: "https://researchr.org/alias/manuel-costa" - name: "Engin Kirda" link: "https://researchr.org/alias/engin-kirda" publisher: "ACM" isbn: "978-1-4503-0059-9" kind: "inproceedings" key: "ReedAWHPS10" - title: "Higher-Order Subtyping" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Martin Steffen" link: "https://researchr.org/alias/martin-steffen" year: "1997" doi: "http://dx.doi.org/10.1016/S0304-3975(96)00096-5" links: doi: "http://dx.doi.org/10.1016/S0304-3975(96)00096-5" tags: - "C++" - "subtyping" researchr: "https://researchr.org/publication/PierceS97" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "176" number: "1-2" pages: "235-282" kind: "article" key: "PierceS97" - title: "Types and Programming Languages" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2002" abstract: "A type system is a syntactic method for enforcing levels of abstraction in programs. The study of type systems--and of programming languages from a type-theoretic perspective--has important applications in software engineering, language design, high-performance compilers, and security. This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Each chapter is accompanied by numerous exercises and solutions, as well as a running implementation. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material. The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators. Extended case studies develop a variety of approaches to modeling the features of object-oriented languages." tags: - "programming languages" - "object-oriented programming" - "design science" - "meta programming" - "case study" - "meta-model" - "modeling language" - "modeling" - "language engineering" - "software language engineering" - "language modeling" - "language design" - "type system" - "software engineering" - "model-driven engineering" - "C++" - "object-role modeling" - "subtyping" - "security" - "e-science" - "compiler" - "programming" - "subject-oriented programming" - "type theory" - "abstraction" - "Meta-Environment" - "design" - "systematic-approach" - "feature-oriented programming" - "meta-objects" researchr: "https://researchr.org/publication/Pierce2002" cites: 0 citedby: 0 address: "Cambridge, Massachusetts" publisher: "MIT Press" kind: "book" key: "Pierce2002" - title: "Contracts made manifest" author: - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Stephanie Weirich" link: "http://www.cis.upenn.edu/~sweirich/" year: "2010" doi: "http://doi.acm.org/10.1145/1706299.1706341" links: doi: "http://doi.acm.org/10.1145/1706299.1706341" tags: - "contracts" - "C++" researchr: "https://researchr.org/publication/GreenbergPW10" cites: 0 citedby: 0 pages: "353-364" booktitle: "Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010" editor: - name: "Manuel V. Hermenegildo" link: "https://researchr.org/alias/manuel-v.-hermenegildo" - name: "Jens Palsberg" link: "https://researchr.org/alias/jens-palsberg" publisher: "ACM" isbn: "978-1-60558-479-9" kind: "inproceedings" key: "GreenbergPW10" - title: "Foundations for Virtual Types" author: - name: "Atsushi Igarashi" link: "https://researchr.org/alias/atsushi-igarashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2002" doi: "http://www.idealibrary.com/links/doi/10.1006/inco.2001.2942" links: doi: "http://www.idealibrary.com/links/doi/10.1006/inco.2001.2942" tags: - "C++" researchr: "https://researchr.org/publication/IgarashiP02" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "175" number: "1" pages: "34-49" kind: "article" key: "IgarashiP02" - title: "Featherwieght Java: A Minimal Core Calculus for Java and GJ" author: - name: "Atsushi Igarashi" link: "https://researchr.org/alias/atsushi-igarashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Philip Wadler" link: "http://homepages.inf.ed.ac.uk/wadler/" year: "1999" doi: "http://doi.acm.org/10.1145/320384.320395" links: doi: "http://doi.acm.org/10.1145/320384.320395" tags: - "Java" - "C++" researchr: "https://researchr.org/publication/IgarashiPW99" cites: 0 citedby: 0 pages: "132-146" booktitle: "OOPSLA" kind: "inproceedings" key: "IgarashiPW99" - title: "Recursive subtyping revealed: functional pearl" author: - name: "Vladimir Gapeyev" link: "https://researchr.org/alias/vladimir-gapeyev" - name: "Michael Y. Levin" link: "https://researchr.org/alias/michael-y.-levin" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2000" doi: "http://doi.acm.org/10.1145/351240.351261" links: doi: "http://doi.acm.org/10.1145/351240.351261" tags: - "C++" - "subtyping" researchr: "https://researchr.org/publication/GapeyevLP00" cites: 0 citedby: 0 pages: "221-231" booktitle: "ICFP" kind: "inproceedings" key: "GapeyevLP00" - title: "Boomerang: resourceful lenses for string data" author: - name: "Aaron Bohannon" link: "https://researchr.org/alias/aaron-bohannon" - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Alexandre Pilkiewicz" link: "https://researchr.org/alias/alexandre-pilkiewicz" - name: "Alan Schmitt" link: "https://researchr.org/alias/alan-schmitt" year: "2008" doi: "http://doi.acm.org/10.1145/1328438.1328487" abstract: "A lens is a bidirectional program. When read from left to right, it denotes an ordinary function that maps inputs to outputs. When read from right to left, it denotes an “update translator” that takes an input together with an updated output and produces a new input that reflects the update. Many variants of this idea have been explored in the literature, but none deal fully with ordered data. If, for example, an update changes the order of a list in the output, the items in the output list and the chunks of the input that generated them can be misaligned, leading to lost or corrupted data. We attack this problem in the context of bidirectional transfor- mations over strings, the primordial ordered data type. We first pro- pose a collection of bidirectional string lens combinators, based on familiar operations on regular transducers (union, concatena- tion, Kleene-star) and with a type system based on regular expres- sions. We then design a new semantic space of dictionary lenses, enriching the lenses of Foster et al. (2007b) with support for two additional combinators for marking “reorderable chunks” and their keys. To demonstrate the effectiveness of these primitives, we de- scribe the design and implementation of Boomerang, a full-blown bidirectional programming language with dictionary lenses at its core. We have used Boomerang to build transformers for complex real-world data formats including the SwissProt genomic database. We formalize the essential property of resourcefulness—the correct use of keys to associate chunks in the input and output—by defining a refined semantic space of quasi-oblivious lenses. Several previously studied properties of lenses turn out to have compact characterizations in this space." links: doi: "http://doi.acm.org/10.1145/1328438.1328487" tags: - "programming languages" - "rule-based" - "data-flow language" - "language design" - "type system" - "data-flow programming" - "data-flow" - "C++" - "lenses" - "programming" - "database" - "context-aware" - "design" researchr: "https://researchr.org/publication/BohannonFPPS08" cites: 0 citedby: 0 pages: "407-419" booktitle: "Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008" editor: - name: "George C. Necula" link: "https://researchr.org/alias/george-c.-necula" - name: "Philip Wadler" link: "http://homepages.inf.ed.ac.uk/wadler/" publisher: "ACM" isbn: "978-1-59593-689-9" kind: "inproceedings" key: "BohannonFPPS08" - title: "A Logic Your Typechecker Can Count On: Unordered Tree Types in Practice" author: - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Alan Schmitt" link: "https://researchr.org/alias/alan-schmitt" year: "2007" doi: "http://www.plan-x-2007.org/plan-x-2007.pdf" links: doi: "http://www.plan-x-2007.org/plan-x-2007.pdf" tags: - "C++" - "logic" researchr: "https://researchr.org/publication/FosterPS07" cites: 0 citedby: 0 pages: "80-90" booktitle: "PLAN-X 2007, Programming Language Technologies for XML, An ACM SIGPLAN Workshop colocated with POPL 2007, Nice, France, January 20, 2007" kind: "inproceedings" key: "FosterPS07" - title: "Software Foundations " author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Chris Casinghino" link: "https://researchr.org/alias/chris-casinghino" - name: "Marco Gaboardi" link: "https://researchr.org/alias/marco-gaboardi" - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: " Cătălin Hriţcu" link: "https://researchr.org/alias/c%C4%83t%C4%83lin-hri%C5%A3cu" - name: "Vilhelm Sjöberg" link: "https://researchr.org/alias/vilhelm-sj%C3%B6berg" - name: " Brent Yorgey" link: "https://researchr.org/alias/brent-yorgey" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Chris Casinghino" link: "https://researchr.org/alias/chris-casinghino" - name: "Marco Gaboardi" link: "https://researchr.org/alias/marco-gaboardi" - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: " Cătălin Hriţcu" link: "https://researchr.org/alias/c%C4%83t%C4%83lin-hri%C5%A3cu" - name: "Vilhelm Sjöberg" link: "https://researchr.org/alias/vilhelm-sj%C3%B6berg" - name: " Brent Yorgey" link: "https://researchr.org/alias/brent-yorgey" year: "2015" links: "url": "http://www.cis.upenn.edu/~bcpierce/sf/index.html" researchr: "https://researchr.org/publication/SoftwareFoundations2015" cites: 0 citedby: 0 kind: "book" key: "SoftwareFoundations2015" - title: "Foundations for Bidirectional Programming" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2009" doi: "http://dx.doi.org/10.1007/978-3-642-02408-5_1" links: doi: "http://dx.doi.org/10.1007/978-3-642-02408-5_1" tags: - "C++" - "programming" researchr: "https://researchr.org/publication/Pierce09-0" cites: 0 citedby: 0 pages: "1-3" booktitle: "Theory and Practice of Model Transformations, Second International Conference, ICMT 2009, Zurich, Switzerland, June 29-30, 2009. Proceedings" editor: - name: "Richard F. Paige" link: "http://www-users.cs.york.ac.uk/~paige/" volume: "5563" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-02407-8" kind: "inproceedings" key: "Pierce09-0" - title: "Regular expression types for XML" author: - name: "Haruo Hosoya" link: "https://researchr.org/alias/haruo-hosoya" - name: "Jerome Vouillon" link: "https://researchr.org/alias/jerome-vouillon" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2005" doi: "http://doi.acm.org/10.1145/1053468.1053470" links: doi: "http://doi.acm.org/10.1145/1053468.1053470" tags: - "XML" - "XML Schema" - "C++" researchr: "https://researchr.org/publication/HosoyaVP05" cites: 0 citedby: 1 journal: "ACM Transactions on Programming Languages and Systems" volume: "27" number: "1" pages: "46-90" kind: "article" key: "HosoyaVP05" - title: "Regular Object Types" author: - name: "Vladimir Gapeyev" link: "https://researchr.org/alias/vladimir-gapeyev" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2003" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2743&spage=151" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2743&spage=151" tags: - "meta-model" - "C++" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/GapeyevP03" cites: 0 citedby: 0 pages: "151-175" booktitle: "ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, Germany, July 21-25, 2003, Proceedings" editor: - name: "Luca Cardelli" link: "http://lucacardelli.name" volume: "2743" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-40531-3" kind: "inproceedings" key: "GapeyevP03" - title: "Location-Independent Communication for Mobile Agents: A Two-Level Architecture" author: - name: "Peter Sewell" link: "https://researchr.org/alias/peter-sewell" - name: "Pawel T. Wojciechowski" link: "https://researchr.org/alias/pawel-t.-wojciechowski" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1998" doi: "http://link.springer.de/link/service/series/0558/bibs/1686/16860001.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1686/16860001.htm" tags: - "architecture" - "C++" - "mobile" researchr: "https://researchr.org/publication/SewellWP98" cites: 0 citedby: 0 pages: "1-31" booktitle: "Internet Programming Languages, ICCL 98 Workshop, Chicago, IL, USA, May 13, 1998, Proceedings" editor: - name: "Henri E. Bal" link: "https://researchr.org/alias/henri-e.-bal" - name: "Boumediene Belkhouche" link: "https://researchr.org/alias/boumediene-belkhouche" - name: "Luca Cardelli" link: "http://lucacardelli.name" volume: "1686" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-66673-7" kind: "inproceedings" key: "SewellWP98" - title: "Symmetric lenses" author: - name: "Martin Hofmann" link: "https://researchr.org/alias/martin-hofmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Daniel Wagner" link: "https://researchr.org/alias/daniel-wagner" year: "2011" doi: "http://doi.acm.org/10.1145/1926385.1926428" links: doi: "http://doi.acm.org/10.1145/1926385.1926428" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/HofmannPW11" tags: - "C++" researchr: "https://researchr.org/publication/HofmannPW11" cites: 0 citedby: 0 pages: "371-384" booktitle: "Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011" editor: - name: "Thomas Ball" link: "https://researchr.org/alias/thomas-ball" - name: "Mooly Sagiv" link: "https://researchr.org/alias/mooly-sagiv" publisher: "ACM" isbn: "978-1-4503-0490-0" kind: "inproceedings" key: "HofmannPW11" - title: "PUMP: a programmable unit for metadata processing" author: - name: "Udit Dhawan" link: "https://researchr.org/alias/udit-dhawan" - name: "Nikos Vasilakis" link: "https://researchr.org/alias/nikos-vasilakis" - name: "Raphael Rubin" link: "https://researchr.org/alias/raphael-rubin" - name: "Silviu Chiricescu" link: "https://researchr.org/alias/silviu-chiricescu" - name: "Jonathan M. Smith" link: "https://researchr.org/alias/jonathan-m.-smith" - name: "Thomas F. Knight Jr." link: "https://researchr.org/alias/thomas-f.-knight-jr." - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "André DeHon" link: "https://researchr.org/alias/andr%C3%A9-dehon" year: "2014" doi: "http://doi.acm.org/10.1145/2611765.2611773" links: doi: "http://doi.acm.org/10.1145/2611765.2611773" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/isca/DhawanVRCSKPD14" researchr: "https://researchr.org/publication/DhawanVRCSKPD14" cites: 0 citedby: 0 pages: "8" booktitle: "HASP 2014, Hardware and Architectural Support for Security and Privacy, Minneapolis, MN, USA, June 15, 2014" editor: - name: "Ruby B. Lee" link: "https://researchr.org/alias/ruby-b.-lee" - name: "Weidong Shi" link: "https://researchr.org/alias/weidong-shi" publisher: "ACM" isbn: "978-1-4503-2777-0" kind: "inproceedings" key: "DhawanVRCSKPD14" - title: "A bisimulation for type abstraction and recursion" author: - name: "Eijiro Sumii" link: "https://researchr.org/alias/eijiro-sumii" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2007" doi: "http://doi.acm.org/10.1145/1284320.1284325" links: doi: "http://doi.acm.org/10.1145/1284320.1284325" tags: - "C++" - "abstraction" researchr: "https://researchr.org/publication/SumiiP07%3A0" cites: 0 citedby: 0 journal: "Journal of the ACM" volume: "54" number: "5" pages: "26" kind: "article" key: "SumiiP07:0" - title: "Type-Based Optimization for Regular Patterns" author: - name: "Michael Y. Levin" link: "https://researchr.org/alias/michael-y.-levin" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2005" doi: "http://dx.doi.org/10.1007/11601524_12" links: doi: "http://dx.doi.org/10.1007/11601524_12" tags: - "optimization" - "rule-based" - "C++" researchr: "https://researchr.org/publication/LevinP05" cites: 0 citedby: 0 pages: "184-198" booktitle: "Database Programming Languages, 10th International Symposium, DBPL 2005, Trondheim, Norway, August 28-29, 2005, Revised Selected Papers" editor: - name: "Gavin M. Bierman" link: "https://researchr.org/alias/gavin-m.-bierman" - name: "Christoph Koch" link: "https://researchr.org/alias/christoph-koch" volume: "3774" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-30951-9" kind: "inproceedings" key: "LevinP05" - title: "Quotient lenses" author: - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Alexandre Pilkiewicz" link: "https://researchr.org/alias/alexandre-pilkiewicz" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2008" doi: "http://doi.acm.org/10.1145/1411204.1411257" abstract: "There are now a number of bidirectional programming languages, where every program can be read both as a forward transformation mapping one data structure to another and as a reverse transformation mapping an edited output back to a correspondingly edited input. Besides parsimony—the two related transformations are described by just one expression—such languages are attractive because they promise strong behavioral laws about how the two transformations fit together—e.g., their composition is the identity function. It has repeatedly been observed, however, that such laws are actually a bit too strong: in practice, we do not want them “on the nose,” but only up to some equivalence, allowing inessential details, such as whitespace, to be modified after a round trip. Some bidirectional languages loosen their laws in this way, but only for specific, baked-in equivalences. In this work, we propose a general theory of quotient lenses— bidirectional transformations that are well behaved modulo equivalence relations controlled by the programmer. Semantically, quotient lenses are a natural refinement of lenses, which we have studied in previous work. At the level of syntax, we present a rich set of constructs for programming with canonizers and for quotienting lenses by canonizers. We track equivalences explicitly, with the type of every quotient lens specifying the equivalences it respects. We have implemented quotient lenses as a refinement of the bidirectional string processing language Boomerang. We present a number of useful primitive canonizers for strings, and give a simple extension of Boomerang’s regular-expression-based type system to statically typecheck quotient lenses. The resulting language is an expressive tool for transforming real-world, ad-hoc data formats. We demonstrate the power of our notation by developing an extended example based on the UniProt genome database format and illustrate the generality of our approach by showing how uses of quotienting in other bidirectional languages can be translated into our notation." links: doi: "http://doi.acm.org/10.1145/1411204.1411257" tags: - "control systems" - "programming languages" - "parsimony" - "rule-based" - "bidirectional transformation" - "translation" - "data-flow language" - "refinement" - "transformation language" - "composition" - "type system" - "data-flow programming" - "data-flow" - "C++" - "transformation system" - "lenses" - "programming" - "database" - "type theory" - "systematic-approach" - "transformation" - "program transformation" - "domain-specific language" researchr: "https://researchr.org/publication/FosterPP08" cites: 0 citedby: 0 pages: "383-396" booktitle: "Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008" editor: - name: "James Hook" link: "https://researchr.org/alias/james-hook" - name: "Peter Thiemann" link: "http://www.informatik.uni-freiburg.de/~thiemann/" publisher: "ACM" isbn: "978-1-59593-919-7" kind: "inproceedings" key: "FosterPP08" - title: "All Your IFCException Are Belong to Us" author: - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: "Ben Karel" link: "https://researchr.org/alias/ben-karel" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Greg Morrisett" link: "https://researchr.org/alias/greg-morrisett" year: "2013" doi: "http://doi.ieeecomputersociety.org/10.1109/SP.2013.10" links: doi: "http://doi.ieeecomputersociety.org/10.1109/SP.2013.10" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sp/HritcuGKPM13" researchr: "https://researchr.org/publication/HritcuGKPM13" cites: 0 citedby: 0 pages: "3-17" booktitle: "2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013" publisher: "IEEE Computer Society" isbn: "978-1-4673-6166-8" kind: "inproceedings" key: "HritcuGKPM13" - title: "Intersection Types and Bounded Polymorphism" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1997" tags: - "C++" researchr: "https://researchr.org/publication/Pierce97" cites: 0 citedby: 0 journal: "Mathematical Structures in Computer Science" volume: "7" number: "2" pages: "129-193" kind: "article" key: "Pierce97" - title: "Software Foundations " author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Chris Casinghino" link: "https://researchr.org/alias/chris-casinghino" - name: "Marco Gaboardi" link: "https://researchr.org/alias/marco-gaboardi" - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: " Cătălin Hriţcu" link: "https://researchr.org/alias/c%C4%83t%C4%83lin-hri%C5%A3cu" - name: "Vilhelm Sjöberg" link: "https://researchr.org/alias/vilhelm-sj%C3%B6berg" - name: " Brent Yorgey" link: "https://researchr.org/alias/brent-yorgey" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Chris Casinghino" link: "https://researchr.org/alias/chris-casinghino" - name: "Marco Gaboardi" link: "https://researchr.org/alias/marco-gaboardi" - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: " Cătălin Hriţcu" link: "https://researchr.org/alias/c%C4%83t%C4%83lin-hri%C5%A3cu" - name: "Vilhelm Sjöberg" link: "https://researchr.org/alias/vilhelm-sj%C3%B6berg" - name: " Brent Yorgey" link: "https://researchr.org/alias/brent-yorgey" year: "2015" links: "url": "http://www.cis.upenn.edu/~bcpierce/sf/index.html" researchr: "https://researchr.org/publication/SoftwareFoundations2015" cites: 0 citedby: 0 kind: "book" key: "SoftwareFoundations2015" - title: "Faithful Ideal Models for Recursive Polymorphic Types" author: - name: "Martín Abadi" link: "http://users.soe.ucsc.edu/~abadi/home.html" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Gordon D. Plotkin" link: "http://homepages.inf.ed.ac.uk/gdp/" year: "1989" tags: - "C++" researchr: "https://researchr.org/publication/AbadiPP89" cites: 0 citedby: 0 pages: "216-225" booktitle: "Proceedings, Fourth Annual Symposium on Logic in Computer Science, 5-8 June, 1989, Asilomar Conference Center, Pacific Grove, California, USA" publisher: "IEEE Computer Society" kind: "inproceedings" key: "AbadiPP89" - title: "Proof Assistants as Teaching Assistants: A View from the Trenches" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-14052-5_2" links: doi: "http://dx.doi.org/10.1007/978-3-642-14052-5_2" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/Pierce10" tags: - "proof assistant" - "C++" - "teaching" researchr: "https://researchr.org/publication/Pierce10-0" cites: 0 citedby: 0 pages: "8" booktitle: "Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings" editor: - name: "Matt Kaufmann" link: "https://researchr.org/alias/matt-kaufmann" - name: "Lawrence C. Paulson" link: "https://researchr.org/alias/lawrence-c.-paulson" volume: "6172" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-14051-8" kind: "inproceedings" key: "Pierce10-0" - title: "Art, science, and fear" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2010" doi: "http://doi.acm.org/10.1145/1869459.1869540" links: doi: "http://doi.acm.org/10.1145/1869459.1869540" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/oopsla/Pierce10" tags: - "C++" - "e-science" researchr: "https://researchr.org/publication/Pierce10" cites: 0 citedby: 0 pages: "2" booktitle: "Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno/Tahoe, Nevada, USA" editor: - name: "William R. Cook" link: "http://www.cs.utexas.edu/~wcook/" - name: "Siobhán Clarke" link: "https://www.cs.tcd.ie/Siobhan.Clarke/" - name: "Martin C. Rinard" link: "https://researchr.org/alias/martin-c.-rinard" address: "Reno/Tahoe, Nevada" publisher: "ACM" isbn: "978-1-4503-0203-6" kind: "inproceedings" key: "Pierce10" - title: "Exploiting schemas in data synchronization" author: - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Michael B. Greenwald" link: "https://researchr.org/alias/michael-b.-greenwald" - name: "Christian Kirkegaard" link: "https://researchr.org/alias/christian-kirkegaard" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Alan Schmitt" link: "https://researchr.org/alias/alan-schmitt" year: "2007" doi: "http://dx.doi.org/10.1016/j.jcss.2006.10.024" links: doi: "http://dx.doi.org/10.1016/j.jcss.2006.10.024" tags: - "synchronization" - "XML" - "XML Schema" - "data-flow" - "C++" researchr: "https://researchr.org/publication/FosterGKPS07" cites: 0 citedby: 0 journal: "J. Comput. Syst. Sci." volume: "73" number: "4" pages: "669-689" kind: "article" key: "FosterGKPS07" - title: "On Inner Classes" author: - name: "Atsushi Igarashi" link: "https://researchr.org/alias/atsushi-igarashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2002" doi: "http://dx.doi.org/10.1006/inco.2002.3092" links: doi: "http://dx.doi.org/10.1006/inco.2002.3092" tags: - "C++" researchr: "https://researchr.org/publication/IgarashiP02a" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "177" number: "1" pages: "56-89" kind: "article" key: "IgarashiP02a" - title: "Micro-Policies: Formally Verified, Tag-Based Security Monitors" author: - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Maxime Dénès" link: "https://researchr.org/alias/maxime-d%C3%A9n%C3%A8s" - name: "Nick Giannarakis" link: "https://researchr.org/alias/nick-giannarakis" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Antal Spector-Zabusky" link: "https://researchr.org/alias/antal-spector-zabusky" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" year: "2015" doi: "http://dx.doi.org/10.1109/SP.2015.55" links: doi: "http://dx.doi.org/10.1109/SP.2015.55" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sp/AmorimDGHPST15" researchr: "https://researchr.org/publication/AmorimDGHPST15" cites: 0 citedby: 0 pages: "813-830" booktitle: "2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015" publisher: "IEEE Computer Society" isbn: "978-1-4673-6949-7" kind: "inproceedings" key: "AmorimDGHPST15" - title: "Positive Subtyping" author: - name: "Martin Hofmann" link: "https://researchr.org/alias/martin-hofmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1996" tags: - "C++" - "subtyping" researchr: "https://researchr.org/publication/HofmannP96" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "126" number: "1" pages: "11-33" kind: "article" key: "HofmannP96" - title: "Hardware Support for Safety Interlocks and Introspection" author: - name: "Udit Dhawan" link: "https://researchr.org/alias/udit-dhawan" - name: "Albert Kwon" link: "https://researchr.org/alias/albert-kwon" - name: "Edin Kadric" link: "https://researchr.org/alias/edin-kadric" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Jonathan M. Smith" link: "https://researchr.org/alias/jonathan-m.-smith" - name: "André DeHon" link: "https://researchr.org/alias/andr%C3%A9-dehon" - name: "Gregory Malecha" link: "https://researchr.org/alias/gregory-malecha" - name: "Greg Morrisett" link: "https://researchr.org/alias/greg-morrisett" - name: "Thomas F. Knight Jr." link: "https://researchr.org/alias/thomas-f.-knight-jr." - name: "Andrew Sutherland" link: "https://researchr.org/alias/andrew-sutherland" - name: "Tom Hawkins" link: "https://researchr.org/alias/tom-hawkins" - name: "Amanda Zyxnfryx" link: "https://researchr.org/alias/amanda-zyxnfryx" - name: "David Wittenberg" link: "https://researchr.org/alias/david-wittenberg" - name: "Peter Trei" link: "https://researchr.org/alias/peter-trei" - name: "Sumit Ray" link: "https://researchr.org/alias/sumit-ray" - name: "Greg Sullivan" link: "https://researchr.org/alias/greg-sullivan" year: "2012" doi: "http://doi.ieeecomputersociety.org/10.1109/SASOW.2012.11" links: doi: "http://doi.ieeecomputersociety.org/10.1109/SASOW.2012.11" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/saso/DhawanKKHPSDMMKSHZWTRS12" researchr: "https://researchr.org/publication/DhawanKKHPSDMMKSHZWTRS12" cites: 0 citedby: 0 pages: "1-8" booktitle: "Sixth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW 2012, Lyon, France, September 10-14, 2012" publisher: "IEEE Computer Society" isbn: "978-1-4673-5153-9" kind: "inproceedings" key: "DhawanKKHPSDMMKSHZWTRS12" - title: "Comparing Object Encodings" author: - name: "Kim B. Bruce" link: "https://researchr.org/alias/kim-b.-bruce" - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1997" tags: - "meta-model" - "C++" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/BruceCP97" cites: 0 citedby: 0 pages: "415-438" booktitle: "Theoretical Aspects of Computer Software, Third International Symposium, TACS 97, Sendai, Japan, September 23-26, 1997, Proceedings" editor: - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" - name: "Takayasu Ito" link: "https://researchr.org/alias/takayasu-ito" volume: "1281" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-63388-X" kind: "inproceedings" key: "BruceCP97" - title: "Corrigendum: Decidable Bounded Quantification" author: - name: "Giuseppe Castagna" link: "https://researchr.org/alias/giuseppe-castagna" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1995" tags: - "C++" researchr: "https://researchr.org/publication/CastagnaP95" cites: 0 citedby: 0 pages: "408" booktitle: "POPL" kind: "inproceedings" key: "CastagnaP95" - title: "Agreeing to Agree: Conflict Resolution for Optimistically Replicated Data" author: - name: "Michael B. Greenwald" link: "https://researchr.org/alias/michael-b.-greenwald" - name: "Sanjeev Khanna" link: "https://researchr.org/alias/sanjeev-khanna" - name: "Keshav Kunal" link: "https://researchr.org/alias/keshav-kunal" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Alan Schmitt" link: "https://researchr.org/alias/alan-schmitt" year: "2006" doi: "http://dx.doi.org/10.1007/11864219_19" links: doi: "http://dx.doi.org/10.1007/11864219_19" tags: - "data-flow" - "C++" researchr: "https://researchr.org/publication/GreenwaldKKPS06" cites: 0 citedby: 0 pages: "269-283" booktitle: "Distributed Computing, 20th International Symposium, DISC 2006, Stockholm, Sweden, September 18-20, 2006, Proceedings" editor: - name: "Shlomi Dolev" link: "https://researchr.org/alias/shlomi-dolev" volume: "4167" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-44624-9" kind: "inproceedings" key: "GreenwaldKKPS06" - title: "Reactive noninterference" author: - name: "Aaron Bohannon" link: "https://researchr.org/alias/aaron-bohannon" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Vilhelm Sjöberg" link: "https://researchr.org/alias/vilhelm-sj%C3%A3%C2%B6berg" - name: "Stephanie Weirich" link: "http://www.cis.upenn.edu/~sweirich/" - name: "Steve Zdancewic" link: "https://researchr.org/alias/steve-zdancewic" year: "2009" doi: "http://doi.acm.org/10.1145/1653662.1653673" links: doi: "http://doi.acm.org/10.1145/1653662.1653673" tags: - "C++" researchr: "https://researchr.org/publication/BohannonPSWZ09" cites: 0 citedby: 0 pages: "79-90" booktitle: "Proceedings of the 2009 ACM Conference on Computer and Communications Security, CCS 2009, Chicago, Illinois, USA, November 9-13, 2009" editor: - name: "Ehab Al-Shaer" link: "https://researchr.org/alias/ehab-al-shaer" - name: "Somesh Jha" link: "https://researchr.org/alias/somesh-jha" - name: "Angelos D. Keromytis" link: "https://researchr.org/alias/angelos-d.-keromytis" publisher: "ACM" isbn: "978-1-60558-894-0" kind: "inproceedings" key: "BohannonPSWZ09" - title: "Guest editorial" author: - name: "Kathleen Fisher" link: "https://researchr.org/alias/kathleen-fisher" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2002" doi: "http://doi.acm.org/10.1145/514952.514953" links: doi: "http://doi.acm.org/10.1145/514952.514953" tags: - "C++" researchr: "https://researchr.org/publication/FisherP02" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "24" number: "2" pages: "111" kind: "article" key: "FisherP02" - title: "Foundations for Virtual Types" author: - name: "Atsushi Igarashi" link: "https://researchr.org/alias/atsushi-igarashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1999" doi: "http://link.springer.de/link/service/series/0558/bibs/1628/16280161.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1628/16280161.htm" tags: - "C++" researchr: "https://researchr.org/publication/IgarashiP99" cites: 0 citedby: 0 pages: "161-185" booktitle: "ECOOP 99 - Object-Oriented Programming, 13th European Conference, Lisbon, Portugal, June 14-18, 1999, Proceedings" editor: - name: "Rachid Guerraoui" link: "https://researchr.org/alias/rachid-guerraoui" volume: "1628" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-66156-5" kind: "inproceedings" key: "IgarashiP99" - title: "Intersection Types and Bounded Polymorphism" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1993" tags: - "C++" researchr: "https://researchr.org/publication/Pierce93" cites: 0 citedby: 0 pages: "346-360" booktitle: "Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA 93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings" editor: - name: "Marc Bezem" link: "http://www.ii.uib.no/~bezem/" - name: "Jan Friso Groote" link: "http://www.win.tue.nl/~jfg/" volume: "664" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-56517-5" kind: "inproceedings" key: "Pierce93" - title: "On Inner Classes" author: - name: "Atsushi Igarashi" link: "https://researchr.org/alias/atsushi-igarashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2000" doi: "http://link.springer.de/link/service/series/0558/bibs/1850/18500129.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1850/18500129.htm" tags: - "C++" researchr: "https://researchr.org/publication/IgarashiP00" cites: 0 citedby: 0 pages: "129-153" booktitle: "ECOOP 2000 - Object-Oriented Programming, 14th European Conference, Sophia Antipolis and Cannes, France, June 12-16, 2000, Proceedings" editor: - name: "Elisa Bertino" link: "https://researchr.org/alias/elisa-bertino" volume: "1850" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-67660-0" kind: "inproceedings" key: "IgarashiP00" - title: "Featherweight Firefox: Formalizing the Core of a Web Browser" author: - name: "Aaron Bohannon" link: "https://researchr.org/alias/aaron-bohannon" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2010" doi: "https://www.usenix.org/conference/webapps-10/featherweight-firefox-formalizing-core-web-browser" links: doi: "https://www.usenix.org/conference/webapps-10/featherweight-firefox-formalizing-core-web-browser" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/webapps/BohannonP10" researchr: "https://researchr.org/publication/BohannonP10" cites: 0 citedby: 0 booktitle: "USENIX Conference on Web Application Development, WebApps'10, Boston, Massachusetts, USA, June 23-24, 2010" editor: - name: "John K. Ousterhout" link: "https://researchr.org/alias/john-k.-ousterhout" publisher: "USENIX Association" kind: "inproceedings" key: "BohannonP10" - title: "Preface" author: - name: "Matthew Flatt" link: "http://www.cs.utah.edu/~mflatt/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2007" doi: "http://dx.doi.org/10.1017/S0956796807006454" links: doi: "http://dx.doi.org/10.1017/S0956796807006454" tags: - "C++" researchr: "https://researchr.org/publication/FlattP07" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "17" number: "4-5" pages: "431" kind: "article" key: "FlattP07" - title: "Foundational Property-Based Testing" author: - name: "Zoe Paraskevopoulou" link: "https://researchr.org/alias/zoe-paraskevopoulou" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Maxime Dénès" link: "https://researchr.org/alias/maxime-d%C3%A9n%C3%A8s" - name: "Leonidas Lampropoulos" link: "https://researchr.org/alias/leonidas-lampropoulos" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2015" doi: "http://dx.doi.org/10.1007/978-3-319-22102-1_22" links: doi: "http://dx.doi.org/10.1007/978-3-319-22102-1_22" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/Paraskevopoulou15" researchr: "https://researchr.org/publication/Paraskevopoulou15" cites: 0 citedby: 0 pages: "325-343" booktitle: "Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings" editor: - name: "Christian Urban" link: "https://researchr.org/alias/christian-urban" - name: "Xingyuan Zhang" link: "https://researchr.org/alias/xingyuan-zhang" volume: "9236" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-22101-4" kind: "inproceedings" key: "Paraskevopoulou15" - title: "Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation" author: - name: "Yannis Juglaret" link: "https://researchr.org/alias/yannis-juglaret" - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Boris Eng" link: "https://researchr.org/alias/boris-eng" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2016" doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2016.11" links: doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2016.11" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csfw/JuglaretHAEP16" researchr: "https://researchr.org/publication/JuglaretHAEP16" cites: 0 citedby: 0 pages: "45-60" booktitle: "IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016" publisher: "IEEE" isbn: "978-1-5090-2607-4" kind: "inproceedings" key: "JuglaretHAEP16" - title: "The essence of objects" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2000" doi: "http://doi.acm.org/10.1145/340855.340989" links: doi: "http://doi.acm.org/10.1145/340855.340989" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/sigsoft/Pierce00" researchr: "https://researchr.org/publication/Pierce00" cites: 0 citedby: 0 journal: "ACM SIGSOFT Software Engineering Notes" volume: "25" number: "1" pages: "69-71" kind: "article" key: "Pierce00" - title: "XDuce: A Typed XML Processing Language (Preliminary Report)" author: - name: "Haruo Hosoya" link: "https://researchr.org/alias/haruo-hosoya" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2000" doi: "http://www.research.att.com/conf/webdb2000/PAPERS/7c.ps" links: doi: "http://www.research.att.com/conf/webdb2000/PAPERS/7c.ps" tags: - "XML" - "XML Schema" - "C++" researchr: "https://researchr.org/publication/HosoyaP00" cites: 0 citedby: 0 pages: "111-116" booktitle: "The World Wide Web and Databases, Third International Workshop WebDB 2000, Dallas, Texas, USA, Maaay 18-19, 2000, Selected Papers" editor: - name: "Dan Suciu" link: "https://researchr.org/alias/dan-suciu" - name: "Gottfried Vossen" link: "https://researchr.org/alias/gottfried-vossen" volume: "1997" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-41826-1" kind: "inproceedings" key: "HosoyaP00" - title: "Preface" author: - name: "Uwe Nestmann" link: "https://researchr.org/alias/uwe-nestmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1998" doi: "http://www.elsevier.com/gej-ng/31/29/23/40/26/show/Products/notes/index.htt#001" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/40/26/show/Products/notes/index.htt#001" tags: - "C++" researchr: "https://researchr.org/publication/NestmannP98" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "16" number: "3" pages: "291" kind: "article" key: "NestmannP98" - title: "Foundations of Object-Oriented Languages - Introduction" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1999" tags: - "meta-model" - "C++" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/Pierce99" cites: 0 citedby: 0 journal: "TAPOS" volume: "5" number: "1" pages: "1" kind: "article" key: "Pierce99" - title: "XTATIC" author: - name: "Vladimir Gapeyev" link: "https://researchr.org/alias/vladimir-gapeyev" - name: "Michael Y. Levin" link: "https://researchr.org/alias/michael-y.-levin" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Alan Schmitt" link: "https://researchr.org/alias/alan-schmitt" year: "2006" tags: - "C++" researchr: "https://researchr.org/publication/GapayevLPS06" cites: 0 citedby: 0 pages: "88" booktitle: "PLAN-X 2006 Informal Proceedings, Charleston, South Carolina, January 14, 2006" editor: - name: "Giuseppe Castagna" link: "https://researchr.org/alias/giuseppe-castagna" - name: "Mukund Raghavachari" link: "https://researchr.org/alias/mukund-raghavachari" publisher: "BRICS, Department of Computer Science, University of Aarhus" kind: "inproceedings" key: "GapayevLPS06" - title: "Dynamic Typing in a Statically Typed Language" author: - name: "Martín Abadi" link: "http://users.soe.ucsc.edu/~abadi/home.html" - name: "Luca Cardelli" link: "http://lucacardelli.name" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Gordon D. Plotkin" link: "http://homepages.inf.ed.ac.uk/gdp/" year: "1991" doi: "http://doi.acm.org/10.1145/103135.103138" links: doi: "http://doi.acm.org/10.1145/103135.103138" tags: - "C++" researchr: "https://researchr.org/publication/AbadiCPP91" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "13" number: "2" pages: "237-268" kind: "article" key: "AbadiCPP91" - title: "Pict: a programming language based on the Pi-Calculus" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "David N. Turner" link: "https://researchr.org/alias/david-n.-turner" year: "2000" tags: - "programming languages" - "rule-based" - "C++" - "programming" researchr: "https://researchr.org/publication/PierceT00" cites: 0 citedby: 0 pages: "455-494" booktitle: "Proof, Language, and Interaction, Essays in Honour of Robin Milner" editor: - name: "Gordon D. Plotkin" link: "https://researchr.org/alias/gordon-d.-plotkin" - name: "Colin Stirling" link: "https://researchr.org/alias/colin-stirling" - name: "Mads Tofte" link: "https://researchr.org/alias/mads-tofte" publisher: "The MIT Press" isbn: "978-0-262-16188-6" kind: "inproceedings" key: "PierceT00" - title: "A framework for adaptive differential privacy" author: - name: "Daniel Winograd-Cort" link: "https://researchr.org/alias/daniel-winograd-cort" - name: "Andreas Haeberlen" link: "https://researchr.org/alias/andreas-haeberlen" - name: "Aaron Roth" link: "https://researchr.org/alias/aaron-roth" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2017" doi: "http://doi.acm.org/10.1145/3110254" links: doi: "http://doi.acm.org/10.1145/3110254" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/Winograd-CortHR17" researchr: "https://researchr.org/publication/Winograd-CortHR17" cites: 0 citedby: 0 journal: "Proceedings of the ACM on Programming Languages" volume: "1" number: "ICFP" kind: "article" key: "Winograd-CortHR17" - title: "A bisimulation for dynamic sealing" author: - name: "Eijiro Sumii" link: "https://researchr.org/alias/eijiro-sumii" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2007" doi: "http://dx.doi.org/10.1016/j.tcs.2006.12.032" links: doi: "http://dx.doi.org/10.1016/j.tcs.2006.12.032" tags: - "C++" researchr: "https://researchr.org/publication/SumiiP07" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "375" number: "1-3" pages: "169-192" kind: "article" key: "SumiiP07" - title: "Synthesizing bijective lenses" author: - name: "Anders Miltner" link: "https://researchr.org/alias/anders-miltner" - name: "Kathleen Fisher" link: "https://researchr.org/alias/kathleen-fisher" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "David Walker" link: "https://researchr.org/alias/david-walker" - name: "Steve Zdancewic" link: "https://researchr.org/alias/steve-zdancewic" year: "2018" doi: "http://doi.acm.org/10.1145/3158089" links: doi: "http://doi.acm.org/10.1145/3158089" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/MiltnerFPWZ18" researchr: "https://researchr.org/publication/MiltnerFPWZ18" cites: 0 citedby: 0 journal: "Proceedings of the ACM on Programming Languages" volume: "2" number: "POPL" kind: "article" key: "MiltnerFPWZ18" - title: "Linearity and the Pi-Calculus" author: - name: "Naoki Kobayashi" link: "https://researchr.org/alias/naoki-kobayashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "David N. Turner" link: "https://researchr.org/alias/david-n.-turner" year: "1996" doi: "http://doi.acm.org/10.1145/237721.237804" links: doi: "http://doi.acm.org/10.1145/237721.237804" tags: - "C++" researchr: "https://researchr.org/publication/KobayashiPT96" cites: 0 citedby: 0 pages: "358-371" booktitle: "POPL" kind: "inproceedings" key: "KobayashiPT96" - title: "Bounded Quantification is Undecidable" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1994" month: "July" tags: - "C++" researchr: "https://researchr.org/publication/Pierce94%3A1" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "112" number: "1" pages: "131-165" kind: "article" key: "Pierce94:1" - title: "Type Destructors" author: - name: "Martin Hofmann" link: "https://researchr.org/alias/martin-hofmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2002" doi: "http://www.idealibrary.com/links/doi:10.1006/inco.2001.2926" links: doi: "http://www.idealibrary.com/links/doi:10.1006/inco.2001.2926" tags: - "C++" researchr: "https://researchr.org/publication/HofmannP02" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "172" number: "1" pages: "29-62" kind: "article" key: "HofmannP02" - title: "Regular expression pattern matching for XML" author: - name: "Haruo Hosoya" link: "https://researchr.org/alias/haruo-hosoya" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2003" doi: "http://dx.doi.org/10.1017/S0956796802004410" links: doi: "http://dx.doi.org/10.1017/S0956796802004410" tags: - "XML" - "XML Schema" - "C++" - "pattern matching" researchr: "https://researchr.org/publication/HosoyaP03" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "13" number: "6" pages: "961-1004" kind: "article" key: "HosoyaP03" - title: "Statically Typed Document Transformation: An Xtatic Experience" author: - name: "Vladimir Gapeyev" link: "https://researchr.org/alias/vladimir-gapeyev" - name: "François Garillot" link: "https://researchr.org/alias/fran%C3%A7ois-garillot" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2006" tags: - "C++" - "transformation" researchr: "https://researchr.org/publication/GapeyevGP06" cites: 0 citedby: 0 pages: "2-13" booktitle: "PLAN-X 2006 Informal Proceedings, Charleston, South Carolina, January 14, 2006" editor: - name: "Giuseppe Castagna" link: "https://researchr.org/alias/giuseppe-castagna" - name: "Mukund Raghavachari" link: "https://researchr.org/alias/mukund-raghavachari" publisher: "BRICS, Department of Computer Science, University of Aarhus" kind: "inproceedings" key: "GapeyevGP06" - title: "Featherweight Java: a minimal core calculus for Java and GJ" author: - name: "Atsushi Igarashi" link: "https://researchr.org/alias/atsushi-igarashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Philip Wadler" link: "http://homepages.inf.ed.ac.uk/wadler/" year: "2001" doi: "http://doi.acm.org/10.1145/503502.503505" links: doi: "http://doi.acm.org/10.1145/503502.503505" tags: - "Java" - "C++" researchr: "https://researchr.org/publication/IgarashiPW01" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "23" number: "3" pages: "396-450" kind: "article" key: "IgarashiPW01" - title: "Linearity and the pi-calculus" author: - name: "Naoki Kobayashi" link: "https://researchr.org/alias/naoki-kobayashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "David N. Turner" link: "https://researchr.org/alias/david-n.-turner" year: "1999" doi: "http://doi.acm.org/10.1145/330249.330251" links: doi: "http://doi.acm.org/10.1145/330249.330251" tags: - "C++" researchr: "https://researchr.org/publication/KobayashiPT99" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "21" number: "5" pages: "914-947" kind: "article" key: "KobayashiPT99" - title: "A Unifying Type-Theoretic Framework for Objects" author: - name: "Martin Hofmann" link: "https://researchr.org/alias/martin-hofmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1995" tags: - "meta-model" - "C++" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/HofmannP95" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "5" number: "4" pages: "593-635" kind: "article" key: "HofmannP95" - title: "Local type inference" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "David N. Turner" link: "https://researchr.org/alias/david-n.-turner" year: "2000" doi: "http://doi.acm.org/10.1145/345099.345100" abstract: "We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, without long-distance constraints such as unification variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound variables in function abstractions by propagating type constraints downward from enclosing application nodes. We motivate our design choices by a statistical analysis of the uses of type inference in a sizable body of existing ML code." links: doi: "http://doi.acm.org/10.1145/345099.345100" tags: - "type inference" - "language design" - "constraints" - "C++" - "subtyping" - "abstraction" - "local type inference" researchr: "https://researchr.org/publication/PierceT-TOPLAS-2000" cites: 54 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "22" number: "1" pages: "1-44" kind: "article" key: "PierceT-TOPLAS-2000" - title: "Typing and Subtyping for Mobile Processes" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Davide Sangiorgi" link: "https://researchr.org/alias/davide-sangiorgi" year: "1996" tags: - "C++" - "subtyping" - "mobile" researchr: "https://researchr.org/publication/PierceS96" cites: 0 citedby: 0 journal: "Mathematical Structures in Computer Science" volume: "6" number: "5" pages: "409-453" kind: "article" key: "PierceS96" - title: "Decoding Choice Encodings" author: - name: "Uwe Nestmann" link: "https://researchr.org/alias/uwe-nestmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2000" tags: - "C++" researchr: "https://researchr.org/publication/NestmannP00" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "163" number: "1" pages: "1-59" kind: "article" key: "NestmannP00" - title: "Higher-Order Subtyping" author: - name: "Martin Steffen" link: "https://researchr.org/alias/martin-steffen" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "1994" tags: - "C++" - "subtyping" researchr: "https://researchr.org/publication/SteffenP94" cites: 0 citedby: 0 pages: "511-530" booktitle: "Programming Concepts, Methods and Calculi, Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET 94) San Miniato, Italy, 6-10 June, 1994" editor: - name: "Ernst-Rüdiger Olderog" link: "https://researchr.org/alias/ernst-r%C3%BCdiger-olderog" volume: "A-56" series: "IFIP Transactions" publisher: "North-Holland" isbn: "0-444-82020-5" kind: "inproceedings" key: "SteffenP94" - title: "Edit lenses" author: - name: "Martin Hofmann" link: "https://researchr.org/alias/martin-hofmann" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Daniel Wagner" link: "https://researchr.org/alias/daniel-wagner" year: "2012" doi: "http://doi.acm.org/10.1145/2103656.2103715" links: doi: "http://doi.acm.org/10.1145/2103656.2103715" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/HofmannPW12" researchr: "https://researchr.org/publication/HofmannPW12" cites: 0 citedby: 0 pages: "495-508" booktitle: "Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012" editor: - name: "John Field" link: "https://researchr.org/alias/john-field" - name: "Michael Hicks" link: "https://researchr.org/alias/michael-hicks" publisher: "ACM" isbn: "978-1-4503-1083-3" kind: "inproceedings" key: "HofmannPW12" - title: "Guest editorial" author: - name: "Martin Odersky" link: "http://lampwww.epfl.ch/~odersky/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2004" doi: "http://doi.acm.org/10.1145/1018203.1018204" links: doi: "http://doi.acm.org/10.1145/1018203.1018204" tags: - "C++" researchr: "https://researchr.org/publication/OderskyP04" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "26" number: "5" pages: "767-768" kind: "article" key: "OderskyP04" - title: "Contracts made manifest" author: - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" year: "2012" doi: "http://dx.doi.org/10.1017/S0956796812000135" links: doi: "http://dx.doi.org/10.1017/S0956796812000135" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/GreenbergPW12" researchr: "https://researchr.org/publication/GreenbergPW12" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "22" number: "3" pages: "225-274" kind: "article" key: "GreenbergPW12" - title: "Engineering formal metatheory" author: - name: "Brian E. Aydemir" link: "https://researchr.org/alias/brian-e.-aydemir" - name: "Arthur Charguéraud" link: "https://researchr.org/alias/arthur-chargu%C3%A9raud" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Randy Pollack" link: "https://researchr.org/alias/randy-pollack" - name: "Stephanie Weirich" link: "http://www.cis.upenn.edu/~sweirich/" year: "2008" doi: "http://doi.acm.org/10.1145/1328438.1328443" abstract: "Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. The representation and manipulation of terms with variable binding is a key issue. We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductive definitions of relations on terms (typing, reduction, ...). The key technical insight is that our use of cofinite quantification obviates the need for reasoning about equivariance (the fact that free names can be renamed in derivations); in particular, the structural induction principles of relations defined using cofinite quantification are strong enough for metatheoretic reasoning, and need not be explicitly strengthened. Strong inversion principles follow (automatically, in Coq) from the induction principles. Although many of the underlying ingredients of our technique have been used before, their combination here yields a significant improvement over existing methodology, leading to developments that are faithful to informal practice, yet require no external tool support and little infrastructure within the proof assistant. We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for and ML (with references, exceptions, datatypes, recursion and patterns) and subject reduction for the Calculus of Constructions. Not only do these developments demonstrate the comprehensiveness of our approach; they have also been optimized for clarity and robustness, making them good templates for future extension. " links: doi: "http://doi.acm.org/10.1145/1328438.1328443" tags: - "programming languages" - "optimization" - "object-oriented programming" - "Machanized Metatheory" - "proof assistant" - "pattern language" - "type soundness" - "exceptions" - "Coq" - "variable binding" - "language engineering" - "Cofinite quantification" - "principles" - "little language" - "C++" - "metatheory" - "programming" - "subject-oriented programming" - "Syntactic type soundness" - "program optimization" - "systematic-approach" - "feature-oriented programming" - "Locally nameless" researchr: "https://researchr.org/publication/AydemirCPPW08" cites: 0 citedby: 0 pages: "3-15" booktitle: "Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008" editor: - name: "George C. Necula" link: "https://researchr.org/alias/george-c.-necula" - name: "Philip Wadler" link: "http://homepages.inf.ed.ac.uk/wadler/" publisher: "ACM" isbn: "978-1-59593-689-9" kind: "inproceedings" key: "AydemirCPPW08" - title: "Adventures in Bidirectional Programming" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2007" doi: "http://dx.doi.org/10.1007/978-3-540-77050-3_3" links: doi: "http://dx.doi.org/10.1007/978-3-540-77050-3_3" tags: - "C++" - "programming" researchr: "https://researchr.org/publication/Pierce07" cites: 0 citedby: 0 pages: "21-22" booktitle: "FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, New Delhi, India, December 12-14, 2007, Proceedings" editor: - name: "Vikraman Arvind" link: "https://researchr.org/alias/vikraman-arvind" - name: "Sanjiva Prasad" link: "https://researchr.org/alias/sanjiva-prasad" volume: "4855" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-77049-7" kind: "inproceedings" key: "Pierce07" - title: "Preliminary design of the SAFE platform" author: - name: "André DeHon" link: "https://researchr.org/alias/andr%C3%A9-dehon" - name: "Ben Karel" link: "https://researchr.org/alias/ben-karel" - name: "Thomas F. Knight Jr." link: "https://researchr.org/alias/thomas-f.-knight-jr." - name: "Gregory Malecha" link: "https://researchr.org/alias/gregory-malecha" - name: "Benoît Montagu" link: "https://researchr.org/alias/beno%C3%AEt-montagu" - name: "Robin Morisset" link: "https://researchr.org/alias/robin-morisset" - name: "Greg Morrisett" link: "https://researchr.org/alias/greg-morrisett" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Randy Pollack" link: "https://researchr.org/alias/randy-pollack" - name: "Sumit Ray" link: "https://researchr.org/alias/sumit-ray" - name: "Olin Shivers" link: "https://researchr.org/alias/olin-shivers" - name: "Jonathan M. Smith" link: "https://researchr.org/alias/jonathan-m.-smith" - name: "Gregory Sullivan" link: "https://researchr.org/alias/gregory-sullivan" year: "2011" doi: "http://doi.acm.org/10.1145/2039239.2039245" links: doi: "http://doi.acm.org/10.1145/2039239.2039245" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sosp/DeHonKKMMMMPPRS11" researchr: "https://researchr.org/publication/DeHonKKMMMMPPRS11" cites: 0 citedby: 0 booktitle: "Proceedings of the 6th Workshop on Programming Languages and Operating Systems, PLOS@SOSP 2011, Cascais, Portugal, October 23, 2011" publisher: "ACM" isbn: "978-1-4503-0979-0" kind: "inproceedings" key: "DeHonKKMMMMPPRS11" - title: "Mechanized Metatheory for the Masses: The PoplMark Challenge" author: - name: "Brian E. Aydemir" link: "https://researchr.org/alias/brian-e.-aydemir" - name: "Aaron Bohannon" link: "https://researchr.org/alias/aaron-bohannon" - name: "Matthew Fairbairn" link: "https://researchr.org/alias/matthew-fairbairn" - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Peter Sewell" link: "https://researchr.org/alias/peter-sewell" - name: "Dimitrios Vytiniotis" link: "http://" - name: "Geoffrey Washburn" link: "https://researchr.org/alias/geoffrey-washburn" - name: "Stephanie Weirich" link: "http://www.cis.upenn.edu/~sweirich/" - name: "Steve Zdancewic" link: "https://researchr.org/alias/steve-zdancewic" year: "2005" doi: "http://dx.doi.org/10.1007/11541868_4" abstract: "How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs? We propose an initial set of benchmarks for measuring progress in this area. Based on the metatheory of System F<:, a typed lambda-calculus with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research." links: doi: "http://dx.doi.org/10.1007/11541868_4" tags: - "programming languages" - "rule-based" - "variable binding" - "principles" - "type system" - "C++" - "metatheory" - "subtyping" - "programming" - "state machines" researchr: "https://researchr.org/publication/AydemirBFFPSVWWZ05" cites: 0 citedby: 0 pages: "50-65" booktitle: "Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings" editor: - name: "Joe Hurd" link: "https://researchr.org/alias/joe-hurd" - name: "Thomas F. Melham" link: "https://researchr.org/alias/thomas-f.-melham" volume: "3603" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-28372-2" kind: "inproceedings" key: "AydemirBFFPSVWWZ05" - title: "Typing and Subtyping for Mobile Processes" author: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Davide Sangiorgi" link: "https://researchr.org/alias/davide-sangiorgi" year: "1993" tags: - "C++" - "subtyping" - "mobile" researchr: "https://researchr.org/publication/PierceS93" cites: 0 citedby: 0 pages: "376-385" booktitle: "Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, 19-23 June 1993, Montreal, Canada" publisher: "IEEE Computer Society" kind: "inproceedings" key: "PierceS93" - title: "Matching lenses: alignment and view update" author: - name: "Davi M. J. Barbosa" link: "https://researchr.org/alias/davi-m.-j.-barbosa" - name: "Julien Cretin" link: "https://researchr.org/alias/julien-cretin" - name: "J. Nathan Foster" link: "http://www.cs.princeton.edu/~jnfoster/" - name: "Michael Greenberg" link: "https://researchr.org/alias/michael-greenberg" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2010" doi: "http://doi.acm.org/10.1145/1863543.1863572" links: doi: "http://doi.acm.org/10.1145/1863543.1863572" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/BarbosaCFGP10" tags: - "C++" researchr: "https://researchr.org/publication/BarbosaCFGP10" cites: 0 citedby: 0 pages: "193-204" booktitle: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010" editor: - name: "Paul Hudak" link: "https://researchr.org/alias/paul-hudak" - name: "Stephanie Weirich" link: "https://researchr.org/alias/stephanie-weirich" publisher: "ACM" isbn: "978-1-60558-794-3" kind: "inproceedings" key: "BarbosaCFGP10" - title: "XDuce: A statically typed XML processing language" author: - name: "Haruo Hosoya" link: "https://researchr.org/alias/haruo-hosoya" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" year: "2003" doi: "http://doi.acm.org/10.1145/767193.767195" links: doi: "http://doi.acm.org/10.1145/767193.767195" tags: - "XML" - "XML Schema" - "C++" researchr: "https://researchr.org/publication/HosoyaP03%3A0" cites: 0 citedby: 0 journal: "ACM Trans. Internet Techn." volume: "3" number: "2" pages: "117-148" kind: "article" key: "HosoyaP03:0" - title: "Testing noninterference, quickly" author: - name: "Catalin Hritcu" link: "https://researchr.org/alias/catalin-hritcu" - name: "John Hughes" link: "http://www.cse.chalmers.se/~rjmh" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Antal Spector-Zabusky" link: "https://researchr.org/alias/antal-spector-zabusky" - name: "Dimitrios Vytiniotis" link: "https://researchr.org/alias/dimitrios-vytiniotis" - name: "Arthur Azevedo de Amorim" link: "https://researchr.org/alias/arthur-azevedo-de-amorim" - name: "Leonidas Lampropoulos" link: "https://researchr.org/alias/leonidas-lampropoulos" year: "2013" doi: "http://doi.acm.org/10.1145/2500365.2500574" links: doi: "http://doi.acm.org/10.1145/2500365.2500574" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/HritcuHPSVAL13" researchr: "https://researchr.org/publication/HritcuHPSVAL13" cites: 0 citedby: 0 pages: "455-468" booktitle: "ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013" editor: - name: "Greg Morrisett" link: "https://researchr.org/alias/greg-morrisett" - name: "Tarmo Uustalu" link: "https://researchr.org/alias/tarmo-uustalu" publisher: "ACM" isbn: "978-1-4503-2326-0" kind: "inproceedings" key: "HritcuHPSVAL13" - title: "Dedication" author: - name: "Stephen Brookes" link: "https://researchr.org/alias/stephen-brookes" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Gordon D. Plotkin" link: "https://researchr.org/alias/gordon-d.-plotkin" - name: "Dana S. Scott" link: "https://researchr.org/alias/dana-s.-scott" year: "2013" doi: "http://dx.doi.org/10.1016/j.entcs.2013.09.004" links: doi: "http://dx.doi.org/10.1016/j.entcs.2013.09.004" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/entcs/BrookesPPS13" researchr: "https://researchr.org/publication/BrookesPPS13" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "298" pages: "3-5" kind: "article" key: "BrookesPPS13" - title: "Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009" year: "2009" tags: - "programming languages" - "programming language" - "principles" - "programming" researchr: "https://researchr.org/publication/popl%3A2009" cites: 0 citedby: 0 booktitle: "Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009" conference: "POPL" editor: - name: "Zhong Shao" link: "https://researchr.org/alias/zhong-shao" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "ACM" isbn: "978-1-60558-379-2" kind: "proceedings" key: "popl:2009" - title: "Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012" year: "2012" doi: "http://dl.acm.org/citation.cfm?id=2103786" links: doi: "http://dl.acm.org/citation.cfm?id=2103786" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tldi/2012" researchr: "https://researchr.org/publication/tldi-2012" cites: 0 citedby: 0 booktitle: "Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012" conference: "tldi" editor: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "ACM" isbn: "978-1-4503-1120-5" kind: "proceedings" key: "tldi-2012" - title: "Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), Firenze (Florence), Italy, September 3-5, 2001" year: "2001" note: "SIGPLAN Notices 36(10), October 2001" links: dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/2001" researchr: "https://researchr.org/publication/icfp-2001" cites: 0 citedby: 0 booktitle: "Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), Firenze (Florence), Italy, September 3-5, 2001" conference: "ICFP" editor: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "ACM" isbn: "1-58113-415-0" kind: "proceedings" key: "icfp-2001" - title: "Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings" year: "2001" researchr: "https://researchr.org/publication/tacs%3A2001" cites: 0 citedby: 0 booktitle: "Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings" conference: "tacs" editor: - name: "Naoki Kobayashi" link: "https://researchr.org/alias/naoki-kobayashi" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" volume: "2215" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-42736-8" kind: "proceedings" key: "tacs:2001" - title: "Software Security -- Theories and Systems, Mext-NSF-JSPS International Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002, Revised Papers" year: "2003" tags: - "security" researchr: "https://researchr.org/publication/isss2%3A2002" cites: 0 citedby: 0 booktitle: "Software Security -- Theories and Systems, Mext-NSF-JSPS International Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002, Revised Papers" conference: "isss2" editor: - name: "Mitsuhiro Okada" link: "https://researchr.org/alias/mitsuhiro-okada" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" - name: "Andre Scedrov" link: "https://researchr.org/alias/andre-scedrov" - name: "Hideyuki Tokuda" link: "https://researchr.org/alias/hideyuki-tokuda" - name: "Akinori Yonezawa" link: "https://researchr.org/alias/akinori-yonezawa" volume: "2609" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-00708-3" kind: "proceedings" key: "isss2:2002" - title: "Advanced Topics in Types and Programming Languages" year: "2005" abstract: "The study of type systems for programming languages now touches many areas of computer science, from language design and implementation to software engineering, network security, databases, and analysis of concurrent and distributed systems. This book offers accessible introductions to key ideas in the field, with contributions by experts on each topic. The topics covered include precise type analyses, which extend simple type systems to give them a better grip on the run time behavior of systems; type systems for low-level languages; applications of types to reasoning about computer programs; type theory as a framework for the design of sophisticated module systems; and advanced techniques in ML-style type inference. Advanced Topics in Types and Programming Languages builds on Benjamin Pierce's Types and Programming Languages (MIT Press, 2002); most of the chapters should be accessible to readers familiar with basic notations and techniques of operational semantics and type systems — the material covered in the first half of the earlier book. Advanced Topics in Types and Programming Languages can be used in the classroom and as a resource for professionals. Most chapters include exercises, ranging in difficulty from quick comprehension checks to challenging extensions, many with solutions. " links: "url": "http://www.cis.upenn.edu/~bcpierce/attapl/" tags: - "programming languages" - "semantics" - "design science" - "type inference" - "program comprehension" - "program analysis" - "application framework" - "language engineering" - "software language engineering" - "analysis" - "language design" - "type system" - "software engineering" - "type checking" - "security" - "programming" - "operational semantics" - "type theory" researchr: "https://researchr.org/publication/Pierce05advancedtopics" cites: 0 citedby: 0 editor: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "The MIT Press" isbn: "0-262-16228-8" kind: "book" key: "Pierce05advancedtopics" - title: "Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005" year: "2005" tags: - "functional programming" - "programming" researchr: "https://researchr.org/publication/icfp%3A2005" cites: 0 citedby: 0 booktitle: "Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005" conference: "ICFP" editor: - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "ACM" isbn: "1-59593-064-7" kind: "proceedings" key: "icfp:2005"