publications: - title: "Linear Higher-Order Pre-Unification" author: - name: "Iliano Cervesato" link: "https://researchr.org/alias/iliano-cervesato" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1997" doi: "http://www.computer.org/proceedings/lics/7925/79250422abs.htm" links: doi: "http://www.computer.org/proceedings/lics/7925/79250422abs.htm" researchr: "https://researchr.org/publication/CervesatoP97" cites: 0 citedby: 0 pages: "422-433" booktitle: "LICS" kind: "inproceedings" key: "CervesatoP97" - title: "Higher-Order Abstract Syntax" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Conal Elliott" link: "http://conal.net/" year: "1988" doi: "https://doi.org/10.1145/960116.54010" links: doi: "https://doi.org/10.1145/960116.54010" tags: - "abstract syntax" researchr: "https://researchr.org/publication/PfenningE88" cites: 0 citedby: 0 pages: "199-208" booktitle: "PLDI" kind: "inproceedings" key: "PfenningE88" - title: "A Proof-Carrying File System with Revocable and Use-Once Certificates" author: - name: "Jamie Morgenstern" link: "https://researchr.org/alias/jamie-morgenstern" - name: "Deepak Garg" link: "https://researchr.org/alias/deepak-garg" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2011" doi: "http://dx.doi.org/10.1007/978-3-642-29963-6_5" links: doi: "http://dx.doi.org/10.1007/978-3-642-29963-6_5" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/stm/MorgensternGP11" researchr: "https://researchr.org/publication/MorgensternGP11" cites: 0 citedby: 0 pages: "40-55" booktitle: "Security and Trust Management - 7th International Workshop, STM 2011, Copenhagen, Denmark, June 27-28, 2011, Revised Selected Papers" editor: - name: "Catherine Meadows" link: "https://researchr.org/alias/catherine-meadows" - name: "M. Carmen Fernández Gago" link: "https://researchr.org/alias/m.-carmen-fern%C3%A1ndez-gago" volume: "7170" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-29962-9" kind: "inproceedings" key: "MorgensternGP11" - title: "Optimizing Higher-Order Pattern Unification" author: - name: "Brigitte Pientka" link: "https://researchr.org/alias/brigitte-pientka" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2741&spage=473" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2741&spage=473" tags: - "optimization" researchr: "https://researchr.org/publication/PientkaP03" cites: 0 citedby: 0 pages: "473-487" booktitle: "Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings" editor: - name: "Franz Baader" link: "https://researchr.org/alias/franz-baader" volume: "2741" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-40559-3" kind: "inproceedings" key: "PientkaP03" - title: "Logical approximation for program analysis" author: - name: "Robert J. Simmons" link: "https://researchr.org/alias/robert-j.-simmons" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2011" doi: "http://dx.doi.org/10.1007/s10990-011-9071-2" links: doi: "http://dx.doi.org/10.1007/s10990-011-9071-2" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/lisp/SimmonsP11" researchr: "https://researchr.org/publication/SimmonsP11" cites: 0 citedby: 0 journal: "Higher-Order and Symbolic Computation" volume: "24" number: "1-2" pages: "41-80" kind: "article" key: "SimmonsP11" - title: "A Declarative Alternative to Assert in Logic Programming" author: - name: "Scott Dietzen" link: "https://researchr.org/alias/scott-dietzen" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1991" tags: - "logic programming" - "programming" - "logic" researchr: "https://researchr.org/publication/DietzenP91" cites: 0 citedby: 0 pages: "372-386" booktitle: "ISLP" kind: "inproceedings" key: "DietzenP91" - title: "On the Unification Problem for Cartesian Closed Categories" author: - name: "Paliath Narendran" link: "https://researchr.org/alias/paliath-narendran" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Richard Statman" link: "https://researchr.org/alias/richard-statman" year: "1993" researchr: "https://researchr.org/publication/NarendranPS93" cites: 0 citedby: 0 pages: "57-63" booktitle: "Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, 19-23 June 1993, Montreal, Canada" publisher: "IEEE Computer Society" kind: "inproceedings" key: "NarendranPS93" - title: "On the Unification Problem for Cartesian Closed Categories" author: - name: "Paliath Narendran" link: "https://researchr.org/alias/paliath-narendran" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Richard Statman" link: "https://researchr.org/alias/richard-statman" year: "1997" researchr: "https://researchr.org/publication/NarendranPS97" cites: 0 citedby: 0 journal: "Journal of Symbolic Logic" volume: "62" number: "2" pages: "636-647" kind: "article" key: "NarendranPS97" - title: "Natural Semantics and Some of Its Meta-Theory in Elf" author: - name: "Spiro Michaylov" link: "https://researchr.org/alias/spiro-michaylov" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1991" tags: - "semantics" - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/MichaylovP91" cites: 0 citedby: 0 pages: "299-344" booktitle: "Extensions of Logic Programming, Second International Workshop, ELP 91, Stockholm, Sweden, January 27-29, 1991, Proceedings" editor: - name: "Lars-Henrik Eriksson" link: "https://researchr.org/alias/lars-henrik-eriksson" - name: "Lars Hallnäs" link: "https://researchr.org/alias/lars-halln%C3%A4s" - name: "Peter Schroeder-Heister" link: "https://researchr.org/alias/peter-schroeder-heister" volume: "596" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-55498-X" kind: "inproceedings" key: "MichaylovP91" - title: "Stateful authorization logic - Proof theory and a case study" author: - name: "Deepak Garg" link: "https://researchr.org/alias/deepak-garg" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2012" doi: "http://dx.doi.org/10.3233/JCS-2012-0456" links: doi: "http://dx.doi.org/10.3233/JCS-2012-0456" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jcs/GargP12" researchr: "https://researchr.org/publication/GargP12" cites: 0 citedby: 0 journal: "Journal of Computer Security" volume: "20" number: "4" pages: "353-391" kind: "article" key: "GargP12" - title: "Tutorial on Lambda-Prolog" author: - name: "Amy P. Felty" link: "https://researchr.org/alias/amy-p.-felty" - name: "Elsa L. Gunter" link: "https://researchr.org/alias/elsa-l.-gunter" - name: "Dale Miller" link: "https://researchr.org/alias/dale-miller" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1990" tags: - "Prolog" researchr: "https://researchr.org/publication/FeltyGMP90" cites: 0 citedby: 0 pages: "682" booktitle: "10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings" editor: - name: "Mark E. Stickel" link: "https://researchr.org/alias/mark-e.-stickel" volume: "449" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-52885-7" kind: "inproceedings" key: "FeltyGMP90" - title: "System Description: Twelf - A Meta-Logical Framework for Deductive Systems" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Carsten Schürmann" link: "https://researchr.org/alias/carsten-sch%C3%BCrmann" year: "1999" doi: "http://link.springer.de/link/service/series/0558/bibs/1632/16320202.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1632/16320202.htm" tags: - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/PfenningS99" cites: 0 citedby: 0 pages: "202-206" booktitle: "Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings" editor: - name: "Harald Ganzinger" link: "https://researchr.org/alias/harald-ganzinger" volume: "1632" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-66222-7" kind: "inproceedings" key: "PfenningS99" - title: "Linear Logical Algorithms" author: - name: "Robert J. Simmons" link: "https://researchr.org/alias/robert-j.-simmons" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2008" doi: "http://dx.doi.org/10.1007/978-3-540-70583-3_28" links: doi: "http://dx.doi.org/10.1007/978-3-540-70583-3_28" researchr: "https://researchr.org/publication/SimmonsP08" cites: 0 citedby: 0 pages: "336-347" booktitle: "Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations" editor: - name: "Luca Aceto" link: "http://www2.ru.is/faculty/luca/" - name: "Ivan Damgård" link: "https://researchr.org/alias/ivan-damg%C3%A5rd" - name: "Leslie Ann Goldberg" link: "https://researchr.org/alias/leslie-ann-goldberg" - name: "Magnús M. Halldórsson" link: "https://researchr.org/alias/magn%C3%BAs-m.-halld%C3%B3rsson" - name: "Anna Ingólfsdóttir" link: "https://researchr.org/alias/anna-ing%C3%B3lfsd%C3%B3ttir" - name: "Igor Walukiewicz" link: "https://researchr.org/alias/igor-walukiewicz" volume: "5126" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-70582-6" kind: "inproceedings" key: "SimmonsP08" - title: "A probabilistic language based on sampling functions" author: - name: "Sungwoo Park" link: "https://researchr.org/alias/sungwoo-park" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Sebastian Thrun" link: "https://researchr.org/alias/sebastian-thrun" year: "2008" doi: "http://doi.acm.org/10.1145/1452044.1452048" links: doi: "http://doi.acm.org/10.1145/1452044.1452048" tags: - "rule-based" researchr: "https://researchr.org/publication/ParkPT08" cites: 0 citedby: 0 journal: "ACM Transactions on Programming Languages and Systems" volume: "31" number: "1" kind: "article" key: "ParkPT08" - title: "Towards a type theory of contexts" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2005" doi: "http://doi.acm.org/10.1145/1088454.1088455" links: doi: "http://doi.acm.org/10.1145/1088454.1088455" tags: - "context-aware" - "type theory" researchr: "https://researchr.org/publication/Pfenning05" cites: 0 citedby: 0 pages: "1" booktitle: "ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005" editor: - name: "Randy Pollack" link: "https://researchr.org/alias/randy-pollack" publisher: "ACM" kind: "inproceedings" key: "Pfenning05" - title: "Logical Frameworks" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2001" researchr: "https://researchr.org/publication/Pfenning01" cites: 0 citedby: 0 pages: "1063-1147" booktitle: "Handbook of Automated Reasoning (in 2 volumes)" editor: - name: "John Alan Robinson" link: "https://researchr.org/alias/john-alan-robinson" - name: "Andrei Voronkov" link: "http://www.voronkov.com/" publisher: "Elsevier and MIT Press" isbn: "0-444-50813-9" kind: "incollection" key: "Pfenning01" - title: "Linear logical relations and observational equivalences for session-based concurrency" author: - name: "Jorge A. Pérez" link: "https://researchr.org/alias/jorge-a.-p%C3%A9rez" - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" year: "2014" doi: "http://dx.doi.org/10.1016/j.ic.2014.08.001" links: doi: "http://dx.doi.org/10.1016/j.ic.2014.08.001" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/iandc/PerezCPT14" researchr: "https://researchr.org/publication/PerezCPT14" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "239" pages: "254-302" kind: "article" key: "PerezCPT14" - title: "Compiling the Polymorphic Lambda-Calculus" author: - name: "Spiro Michaylov" link: "https://researchr.org/alias/spiro-michaylov" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1991" tags: - "compiler" researchr: "https://researchr.org/publication/MichaylovP91%3A0" cites: 0 citedby: 0 pages: "285-296" booktitle: "PEPM" kind: "inproceedings" key: "MichaylovP91:0" - title: "Higher-order pattern complement and the strict lambda-calculus" author: - name: "Alberto Momigliano" link: "https://researchr.org/alias/alberto-momigliano" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" doi: "http://doi.acm.org/10.1145/937555.937559" links: doi: "http://doi.acm.org/10.1145/937555.937559" researchr: "https://researchr.org/publication/MomiglianoP03%3A0" cites: 0 citedby: 0 journal: "ACM Trans. Comput. Log." volume: "4" number: "4" pages: "493-529" kind: "article" key: "MomiglianoP03:0" - title: "Single Axioms in the Implicational Propositional Calculus" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1988" researchr: "https://researchr.org/publication/Pfenning88" cites: 0 citedby: 0 pages: "710-713" booktitle: "9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings" editor: - name: "Ewing L. Lusk" link: "https://researchr.org/alias/ewing-l.-lusk" - name: "Ross A. Overbeek" link: "https://researchr.org/alias/ross-a.-overbeek" volume: "310" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-19343-X" kind: "inproceedings" key: "Pfenning88" - title: "A Bidirectional Refinement Type System for LF" author: - name: "William Lovas" link: "https://researchr.org/alias/william-lovas" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2008" doi: "http://dx.doi.org/10.1016/j.entcs.2007.09.021" links: doi: "http://dx.doi.org/10.1016/j.entcs.2007.09.021" tags: - "refinement" - "type system" researchr: "https://researchr.org/publication/LovasP08" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "196" pages: "113-128" kind: "article" key: "LovasP08" - title: "Intersection types and computational effects" author: - name: "Rowan Davies" link: "https://researchr.org/alias/rowan-davies" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2000" doi: "http://doi.acm.org/10.1145/351240.351259" links: doi: "http://doi.acm.org/10.1145/351240.351259" researchr: "https://researchr.org/publication/DaviesP00" cites: 0 citedby: 0 pages: "198-208" booktitle: "ICFP" kind: "inproceedings" key: "DaviesP00" - title: "A Linear Logic of Authorization and Knowledge" author: - name: "Deepak Garg" link: "https://researchr.org/alias/deepak-garg" - name: "Lujo Bauer" link: "https://researchr.org/alias/lujo-bauer" - name: "Kevin D. Bowers" link: "https://researchr.org/alias/kevin-d.-bowers" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Michael K. Reiter" link: "https://researchr.org/alias/michael-k.-reiter" year: "2006" doi: "http://dx.doi.org/10.1007/11863908_19" links: doi: "http://dx.doi.org/10.1007/11863908_19" tags: - "logic" researchr: "https://researchr.org/publication/GargBBPR06" cites: 0 citedby: 0 pages: "297-312" booktitle: "Computer Security - ESORICS 2006, 11th European Symposium on Research in Computer Security, Hamburg, Germany, September 18-20, 2006, Proceedings" editor: - name: "Dieter Gollmann" link: "https://researchr.org/alias/dieter-gollmann" - name: "Jan Meier" link: "https://researchr.org/alias/jan-meier" - name: "Andrei Sabelfeld" link: "https://researchr.org/alias/andrei-sabelfeld" volume: "4189" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-44601-X" kind: "inproceedings" key: "GargBBPR06" - title: "Session-Typed Concurrent Contracts" author: - name: "Hannah Gommerstadt" link: "https://researchr.org/alias/hannah-gommerstadt" - name: "Limin Jia" link: "https://researchr.org/alias/limin-jia" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2018" doi: "https://doi.org/10.1007/978-3-319-89884-1_27" links: doi: "https://doi.org/10.1007/978-3-319-89884-1_27" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/GommerstadtJP18" researchr: "https://researchr.org/publication/GommerstadtJP18" cites: 0 citedby: 0 pages: "771-798" booktitle: "Programming Languages and Systems - 27th European Symposium on Programming, ESOP 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: "Amal Ahmed" link: "https://researchr.org/alias/amal-ahmed" volume: "10801" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-89884-1" kind: "inproceedings" key: "GommerstadtJP18" - title: "The Practice of Logical Frameworks" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1996" researchr: "https://researchr.org/publication/Pfenning96" cites: 0 citedby: 0 pages: "119-134" booktitle: "Trees in Algebra and Programming - CAAP 96, 21st International Colloquium, Linköping, Sweden, April, 22-24, 1996, Proceedings" editor: - name: "Hélène Kirchner" link: "https://researchr.org/alias/h%C3%A9l%C3%A8ne-kirchner" volume: "1059" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-61064-2" kind: "inproceedings" key: "Pfenning96" - title: "Mode and Termination Checking for Higher-Order Logic Programs" author: - name: "Ekkehard Rohwedder" link: "https://researchr.org/alias/ekkehard-rohwedder" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1996" tags: - "termination" - "logic programming" - "logic" researchr: "https://researchr.org/publication/RohwedderP96" cites: 0 citedby: 0 pages: "296-310" booktitle: "Programming Languages and Systems - ESOP 96, 6th European Symposium on Programming, Linköping, Sweden, April 22-24, 1996, Proceedings" editor: - name: "Hanne Riis Nielson" link: "https://researchr.org/alias/hanne-riis-nielson" volume: "1058" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-61055-3" kind: "inproceedings" key: "RohwedderP96" - title: "Type-Directed Concurrency" author: - name: "Deepak Garg" link: "http://www.cs.cmu.edu/~dg" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2005" doi: "http://dx.doi.org/10.1007/11539452_5" links: doi: "http://dx.doi.org/10.1007/11539452_5" researchr: "https://researchr.org/publication/GargP05" cites: 0 citedby: 0 pages: "6-20" booktitle: "CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings" editor: - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" - name: "Luca de Alfaro" link: "https://researchr.org/alias/luca-de-alfaro" volume: "3653" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-28309-9" kind: "inproceedings" key: "GargP05" - title: "Reasoning about Staged Computation" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2000" doi: "http://link.springer.de/link/service/series/0558/bibs/1924/19240005.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1924/19240005.htm" tags: - "staged computation" researchr: "https://researchr.org/publication/Pfenning00" cites: 0 citedby: 0 pages: "5-6" booktitle: "Semantics, Applications, and Implementation of Program Generation, International Workshop SAIG 2000, Montreal, Canada, September 20, 2000, Proceedings" editor: - name: "Walid Taha" link: "http://www.cs.rice.edu/~taha/" volume: "1924" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-41054-6" kind: "inproceedings" key: "Pfenning00" - title: "The Ergo Support System: An Integrated Set of Tools for Prototyping Integrated Environments" author: - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Gene Rollins" link: "https://researchr.org/alias/gene-rollins" - name: "William L. Scherlis" link: "https://researchr.org/alias/william-l.-scherlis" year: "1988" tags: - "Meta-Environment" researchr: "https://researchr.org/publication/LeePRS88" cites: 0 citedby: 0 pages: "25-34" booktitle: "Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments" address: "New York, USA" publisher: "ACM" kind: "inproceedings" key: "LeePRS88" - title: "The Relative Complement Problem for Higher-Order Patterns" author: - name: "Alberto Momigliano" link: "https://researchr.org/alias/alberto-momigliano" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1999" researchr: "https://researchr.org/publication/MomiglianoP99" cites: 0 citedby: 0 pages: "497-512" booktitle: "1999 Joint Conference on Declarative Programming, AGP 99, L Aquila, Italy, September 6-9, 1999" editor: - name: "Maria Chiara Meo" link: "https://researchr.org/alias/maria-chiara-meo" - name: "Manuel Vilares Ferro" link: "https://researchr.org/alias/manuel-vilares-ferro" kind: "inproceedings" key: "MomiglianoP99" - title: "Manifest Deadlock-Freedom for Shared Session Types" author: - name: "Stephanie Balzer" link: "https://researchr.org/alias/stephanie-balzer" - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2019" doi: "https://doi.org/10.1007/978-3-030-17184-1_22" links: doi: "https://doi.org/10.1007/978-3-030-17184-1_22" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/BalzerTP19" researchr: "https://researchr.org/publication/BalzerTP19" cites: 0 citedby: 0 pages: "611-639" booktitle: "Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings" editor: - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" volume: "11423" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-030-17184-1" kind: "inproceedings" key: "BalzerTP19" - title: "Behavioral Polymorphism and Parametricity in Session-Based Communication" author: - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Jorge A. Pérez" link: "https://researchr.org/alias/jorge-a.-p%C3%A9rez" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-642-37036-6_19" links: doi: "http://dx.doi.org/10.1007/978-3-642-37036-6_19" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/CairesPPT13" researchr: "https://researchr.org/publication/CairesPPT13" cites: 0 citedby: 0 pages: "330-349" booktitle: "Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings" editor: - name: "Matthias Felleisen" link: "http://www.ccs.neu.edu/home/matthias/" - name: "Philippa Gardner" link: "https://researchr.org/alias/philippa-gardner" volume: "7792" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-37035-9" kind: "inproceedings" key: "CairesPPT13" - title: "Logical and Meta-Logical Frameworks (Abstract)" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1999" tags: - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/Pfenning99" cites: 0 citedby: 0 pages: "206" booktitle: "Principles and Practice of Declarative Programming, International Conference PPDP 99, Paris, France, September 29 - October 1, 1999, Proceedings" editor: - name: "Gopalan Nadathur" link: "https://researchr.org/alias/gopalan-nadathur" volume: "1702" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-66540-4" kind: "inproceedings" key: "Pfenning99" - title: "Stateful Authorization Logic: - Proof Theory and a Case Study" author: - name: "Deepak Garg" link: "https://researchr.org/alias/deepak-garg" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-22444-7_14" links: doi: "http://dx.doi.org/10.1007/978-3-642-22444-7_14" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/stm/GargP10" researchr: "https://researchr.org/publication/GargP10-0" cites: 0 citedby: 0 pages: "210-225" booktitle: "Security and Trust Management - 6th International Workshop, STM 2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers" editor: - name: "Jorge Cuéllar" link: "https://researchr.org/alias/jorge-cu%C3%A9llar" - name: "Javier Lopez" link: "https://researchr.org/alias/javier-lopez" - name: "Gilles Barthe" link: "https://researchr.org/alias/gilles-barthe" - name: "Alexander Pretschner" link: "https://researchr.org/alias/alexander-pretschner" volume: "6710" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-22443-0" kind: "inproceedings" key: "GargP10-0" - title: "Efficient resource management for linear logic proof search" author: - name: "Iliano Cervesato" link: "https://researchr.org/alias/iliano-cervesato" - name: "Joshua S. Hodas" link: "https://researchr.org/alias/joshua-s.-hodas" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2000" doi: "http://dx.doi.org/10.1016/S0304-3975(99)00173-5" links: doi: "http://dx.doi.org/10.1016/S0304-3975(99)00173-5" tags: - "logic" - "search" researchr: "https://researchr.org/publication/CervesatoHP00" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "232" number: "1-2" pages: "133-163" kind: "article" key: "CervesatoHP00" - title: "Session Types as Intuitionistic Linear Propositions" author: - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-15375-4_16" links: doi: "http://dx.doi.org/10.1007/978-3-642-15375-4_16" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/concur/CairesP10" researchr: "https://researchr.org/publication/CairesP10" cites: 0 citedby: 0 pages: "222-236" booktitle: "CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings" editor: - name: "Paul Gastin" link: "https://researchr.org/alias/paul-gastin" - name: "François Laroussinie" link: "https://researchr.org/alias/fran%C3%A7ois-laroussinie" volume: "6269" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-15374-7" kind: "inproceedings" key: "CairesP10" - title: "Substructural Operational Semantics as Ordered Logic Programming" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Robert J. Simmons" link: "https://researchr.org/alias/robert-j.-simmons" year: "2009" doi: "http://dx.doi.org/10.1109/LICS.2009.8" links: doi: "http://dx.doi.org/10.1109/LICS.2009.8" tags: - "semantics" - "logic programming" - "programming" - "operational semantics" - "logic" researchr: "https://researchr.org/publication/PfenningS09" cites: 0 citedby: 0 pages: "101-110" booktitle: "Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA" publisher: "IEEE Computer Society" isbn: "978-0-7695-3746-7" kind: "inproceedings" key: "PfenningS09" - title: "A Symmetric Modal Lambda Calculus for Distributed Computing" author: - name: "Tom Murphy VII" link: "https://researchr.org/alias/tom-murphy-vii" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2004" doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920286abs.htm" links: doi: "http://csdl.computer.org/comp/proceedings/lics/2004/2192/00/21920286abs.htm" researchr: "https://researchr.org/publication/VIICHP04" cites: 0 citedby: 0 pages: "286-295" booktitle: "19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings" publisher: "IEEE Computer Society" isbn: "0-7695-2192-4" kind: "inproceedings" key: "VIICHP04" - title: "ETPS: A System to Help Students Write Formal Proofs" author: - name: "Peter B. Andrews" link: "https://researchr.org/alias/peter-b.-andrews" - name: "Chad E. Brown" link: "https://researchr.org/alias/chad-e.-brown" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Matthew Bishop" link: "https://researchr.org/alias/matthew-bishop" - name: "Sunil Issar" link: "https://researchr.org/alias/sunil-issar" - name: "Hongwei Xi" link: "http://www.cs.bu.edu/~hwxi/" year: "2004" doi: "http://dx.doi.org/10.1023/B:JARS.0000021871.18776.94" links: doi: "http://dx.doi.org/10.1023/B:JARS.0000021871.18776.94" researchr: "https://researchr.org/publication/AndrewsBPBIX04" cites: 0 citedby: 0 journal: "Journal of Automated Reasoning" volume: "32" number: "1" pages: "75-92" kind: "article" key: "AndrewsBPBIX04" - title: "The Relative Complement Problem for Higher-Order Patterns" author: - name: "Alberto Momigliano" link: "https://researchr.org/alias/alberto-momigliano" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1999" researchr: "https://researchr.org/publication/MomiglianoP99%3A0" cites: 0 citedby: 0 pages: "380-394" booktitle: "ICLP" kind: "inproceedings" key: "MomiglianoP99:0" - title: "A Module System for a Programming Language Based on the LF Logical Framework" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1998" tags: - "programming languages" - "rule-based" - "programming" researchr: "https://researchr.org/publication/HarperP98" cites: 0 citedby: 0 journal: "Journal of Logic and Computation" volume: "8" number: "1" pages: "5-31" kind: "article" key: "HarperP98" - title: "TPS: A Theorem-Proving System for Classical Type Theory" author: - name: "Peter B. Andrews" link: "https://researchr.org/alias/peter-b.-andrews" - name: "Matthew Bishop" link: "https://researchr.org/alias/matthew-bishop" - name: "Sunil Issar" link: "https://researchr.org/alias/sunil-issar" - name: "Dan Nesmith" link: "https://researchr.org/alias/dan-nesmith" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Hongwei Xi" link: "http://www.cs.bu.edu/~hwxi/" year: "1996" tags: - "type system" - "type theory" researchr: "https://researchr.org/publication/AndrewsBINPX96" cites: 0 citedby: 0 journal: "Journal of Automated Reasoning" volume: "16" number: "3" pages: "321-353" kind: "article" key: "AndrewsBINPX96" - title: "Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization" author: - name: "Scott Dietzen" link: "https://researchr.org/alias/scott-dietzen" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1992" tags: - "rule-based" - "modal logic" - "logic" researchr: "https://researchr.org/publication/DietzenP92" cites: 0 citedby: 0 journal: "Machine Learning" volume: "9" pages: "23-55" kind: "article" key: "DietzenP92" - title: "A Modal Analysis of Staged Computation" author: - name: "Rowan Davies" link: "https://researchr.org/alias/rowan-davies" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1996" doi: "http://doi.acm.org/10.1145/237721.237788" links: doi: "http://doi.acm.org/10.1145/237721.237788" tags: - "analysis" - "staged computation" researchr: "https://researchr.org/publication/DaviesP96" cites: 0 citedby: 0 pages: "258-270" booktitle: "POPL" kind: "inproceedings" key: "DaviesP96" - title: "Proof theory and its role in programming language research" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2015" doi: "http://doi.acm.org/10.1145/2792434.2792438" links: doi: "http://doi.acm.org/10.1145/2792434.2792438" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/Pfenning15" researchr: "https://researchr.org/publication/Pfenning15" cites: 0 citedby: 0 pages: "4" booktitle: "Proceedings of the Programming Languages Mentoring Workshop, PLMW@POPL 2015, Mumbai, India, January 14, 2015" publisher: "ACM" isbn: "978-1-4503-3299-6" kind: "inproceedings" key: "Pfenning15" - title: "Automated Theorem Proving in a Simple Meta-Logic for LF" author: - name: "Carsten Schürmann" link: "https://researchr.org/alias/carsten-sch%C3%BCrmann" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1998" doi: "http://link.springer.de/link/service/series/0558/bibs/1421/14210286.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1421/14210286.htm" tags: - "meta-model" - "logic" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/SchurmannP98" cites: 0 citedby: 0 pages: "286-300" booktitle: "Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings" editor: - name: "Claude Kirchner" link: "https://researchr.org/alias/claude-kirchner" - name: "Hélène Kirchner" link: "https://researchr.org/alias/h%C3%A9l%C3%A8ne-kirchner" volume: "1421" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-64675-2" kind: "inproceedings" key: "SchurmannP98" - title: "Possession as Linear Knowledge" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2010" doi: "http://www.easychair.org/publications/?page=73216885" links: doi: "http://www.easychair.org/publications/?page=73216885" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/Pfenning10" researchr: "https://researchr.org/publication/Pfenning10" cites: 0 citedby: 0 pages: "1" booktitle: "3rd International Workshop on Logics, Agents, and Mobility, LAM'10, Edinburgh, UK, July 14, 2010" editor: - name: "Berndt Müller" link: "https://researchr.org/alias/berndt-m%C3%BCller" volume: "7" series: "EPiC Series" publisher: "EasyChair" kind: "inproceedings" key: "Pfenning10" - title: "Elf: A Language for Logic Definition and Verified Metaprogramming" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1989" tags: - "logic" researchr: "https://researchr.org/publication/Pfenning89" cites: 0 citedby: 0 pages: "313-322" 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: "Pfenning89" - title: "A Coverage Checking Algorithm for LF" author: - name: "Carsten Schürmann" link: "https://researchr.org/alias/carsten-sch%C3%BCrmann" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=120" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=120" tags: - "coverage" researchr: "https://researchr.org/publication/SchurmannP03" cites: 0 citedby: 0 pages: "120-135" booktitle: "Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings" editor: - name: "David A. Basin" link: "https://researchr.org/alias/david-a.-basin" - name: "Burkhart Wolff" link: "https://researchr.org/alias/burkhart-wolff" volume: "2758" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-40664-6" kind: "inproceedings" key: "SchurmannP03" - title: "On the Undecidability of Partial Polymorphic Type Reconstruction" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1993" researchr: "https://researchr.org/publication/Pfenning93" cites: 0 citedby: 0 journal: "Fundamenta Informaticae" volume: "19" number: "1/2" pages: "185-199" kind: "article" key: "Pfenning93" - title: "Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic" author: - name: "Sean McLaughlin" link: "https://researchr.org/alias/sean-mclaughlin" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2008" doi: "http://dx.doi.org/10.1007/978-3-540-89439-1_12" links: doi: "http://dx.doi.org/10.1007/978-3-540-89439-1_12" tags: - "logic" researchr: "https://researchr.org/publication/McLaughlinP08" cites: 0 citedby: 0 pages: "174-181" booktitle: "Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings" editor: - name: "Iliano Cervesato" link: "https://researchr.org/alias/iliano-cervesato" - name: "Helmut Veith" link: "https://researchr.org/alias/helmut-veith" - name: "Andrei Voronkov" link: "http://www.voronkov.com/" volume: "5330" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-89438-4" kind: "inproceedings" key: "McLaughlinP08" - title: "LEAP: A Language with Eval And Polymorphism" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" year: "1989" researchr: "https://researchr.org/publication/PfenningL89" cites: 0 citedby: 0 pages: "345-359" booktitle: "TAPSOFT 89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, March 13-17, 1989, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Is" editor: - name: "Josep Díaz" link: "https://researchr.org/alias/josep-d%C3%ADaz" - name: "Fernando Orejas" link: "https://researchr.org/alias/fernando-orejas" volume: "352" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-50940-2" kind: "inproceedings" key: "PfenningL89" - title: "A Focusing Inverse Method Theorem Prover for First-Order Linear Logic" author: - name: "Kaustuv Chaudhuri" link: "https://researchr.org/alias/kaustuv-chaudhuri" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2005" doi: "http://dx.doi.org/10.1007/11532231_6" links: doi: "http://dx.doi.org/10.1007/11532231_6" tags: - "logic" researchr: "https://researchr.org/publication/ChaudhuriP05" cites: 0 citedby: 0 pages: "69-83" booktitle: "Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings" editor: - name: "Robert Nieuwenhuis" link: "https://researchr.org/alias/robert-nieuwenhuis" volume: "3632" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-28005-7" kind: "inproceedings" key: "ChaudhuriP05" - title: "A probabilistic language based upon sampling functions" author: - name: "Sungwoo Park" link: "https://researchr.org/alias/sungwoo-park" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Sebastian Thrun" link: "https://researchr.org/alias/sebastian-thrun" year: "2005" doi: "http://doi.acm.org/10.1145/1040305.1040320" links: doi: "http://doi.acm.org/10.1145/1040305.1040320" tags: - "rule-based" researchr: "https://researchr.org/publication/ParkPT05" cites: 0 citedby: 0 pages: "171-182" 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: "ParkPT05" - title: "Corecursion and Non-divergence in Session-Typed Processes" author: - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2014" doi: "http://dx.doi.org/10.1007/978-3-662-45917-1_11" links: doi: "http://dx.doi.org/10.1007/978-3-662-45917-1_11" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tgc/ToninhoCP14" researchr: "https://researchr.org/publication/ToninhoCP14" cites: 0 citedby: 0 pages: "159-175" booktitle: "Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers" editor: - name: "Matteo Maffei" link: "https://researchr.org/alias/matteo-maffei" - name: "Emilio Tuosto" link: "https://researchr.org/alias/emilio-tuosto" volume: "8902" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-662-45916-4" kind: "inproceedings" key: "ToninhoCP14" - title: "A Linear Logical Framework" author: - name: "Iliano Cervesato" link: "https://researchr.org/alias/iliano-cervesato" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1996" researchr: "https://researchr.org/publication/CervesatoP96" cites: 0 citedby: 0 pages: "264-275" booktitle: "LICS" kind: "inproceedings" key: "CervesatoP96" - title: "Non-Interference in Constructive Authorization Logic" author: - name: "Deepak Garg" link: "https://researchr.org/alias/deepak-garg" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2006" doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.18" links: doi: "http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.18" tags: - "logic" researchr: "https://researchr.org/publication/GargP06" cites: 0 citedby: 0 pages: "283-296" booktitle: "19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), 5-7 July 2006, Venice, Italy" publisher: "IEEE Computer Society" isbn: "0-7695-2615-2" kind: "inproceedings" key: "GargP06" - title: "Dependent Types in Logic Programming" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1992" tags: - "logic programming" - "programming" - "logic" researchr: "https://researchr.org/publication/Pfenning92%3A5" cites: 0 citedby: 0 pages: "285-311" booktitle: "Types in Logic Programming" kind: "incollection" key: "Pfenning92:5" - title: "Reasoning About Deductions in Linear Logic (Abstract of Invited Talk)" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1998" doi: "http://link.springer.de/link/service/series/0558/bibs/1421/14210001.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1421/14210001.htm" tags: - "logic" researchr: "https://researchr.org/publication/Pfenning98" cites: 0 citedby: 0 pages: "1-2" booktitle: "Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings" editor: - name: "Claude Kirchner" link: "https://researchr.org/alias/claude-kirchner" - name: "Hélène Kirchner" link: "https://researchr.org/alias/h%C3%A9l%C3%A8ne-kirchner" volume: "1421" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-64675-2" kind: "inproceedings" key: "Pfenning98" - title: "A judgmental reconstruction of modal logic" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Rowan Davies" link: "https://researchr.org/alias/rowan-davies" year: "2001" tags: - "modal logic" - "logic" researchr: "https://researchr.org/publication/PfenningD01" cites: 0 citedby: 0 journal: "Mathematical Structures in Computer Science" volume: "11" number: "4" pages: "511-540" kind: "article" key: "PfenningD01" - title: "Automated techniques for provably safe mobile code" author: - name: "Christopher Colby" link: "https://researchr.org/alias/christopher-colby" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" tags: - "mobile code" - "mobile" researchr: "https://researchr.org/publication/ColbyCHLP03" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "290" number: "2" pages: "1175-1199" kind: "article" key: "ColbyCHLP03" - title: "TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory" author: - name: "Peter B. Andrews" link: "https://researchr.org/alias/peter-b.-andrews" - name: "Matthew Bishop" link: "https://researchr.org/alias/matthew-bishop" - name: "Sunil Issar" link: "https://researchr.org/alias/sunil-issar" - name: "Dan Nesmith" link: "https://researchr.org/alias/dan-nesmith" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Hongwei Xi" link: "http://www.cs.bu.edu/~hwxi/" year: "1993" tags: - "type theory" researchr: "https://researchr.org/publication/AndrewsBINPX93" cites: 0 citedby: 0 pages: "366-370" booktitle: "Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG 93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings" editor: - name: "Jeffrey J. Joyce" link: "https://researchr.org/alias/jeffrey-j.-joyce" - name: "Carl-Johan H. Seger" link: "https://researchr.org/alias/carl-johan-h.-seger" volume: "780" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-57826-9" kind: "inproceedings" key: "AndrewsBINPX93" - title: "The TPS Theorem Proving System" author: - name: "Peter B. Andrews" link: "https://researchr.org/alias/peter-b.-andrews" - name: "Sunil Issar" link: "https://researchr.org/alias/sunil-issar" - name: "Dan Nesmith" link: "https://researchr.org/alias/dan-nesmith" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1990" researchr: "https://researchr.org/publication/AndrewsINP90" cites: 0 citedby: 0 pages: "641-642" booktitle: "10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings" editor: - name: "Mark E. Stickel" link: "https://researchr.org/alias/mark-e.-stickel" volume: "449" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-52885-7" kind: "inproceedings" key: "AndrewsINP90" - title: "Linear logical approximations" author: - name: "Robert J. Simmons" link: "https://researchr.org/alias/robert-j.-simmons" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2009" doi: "http://doi.acm.org/10.1145/1480945.1480949" links: doi: "http://doi.acm.org/10.1145/1480945.1480949" researchr: "https://researchr.org/publication/SimmonsP09" cites: 0 citedby: 0 pages: "9-20" booktitle: "Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2009, Savannah, GA, USA, January 19-20, 2009" editor: - name: "Germán Puebla" link: "https://researchr.org/alias/germ%C3%A1n-puebla" - name: "Germán Vidal" link: "http://users.dsic.upv.es/~gvidal/" publisher: "ACM" isbn: "978-1-60558-327-3" kind: "inproceedings" key: "SimmonsP09" - title: "An Authorization Logic With Explicit Time" author: - name: "Henry DeYoung" link: "https://researchr.org/alias/henry-deyoung" - name: "Deepak Garg" link: "http://www.cs.cmu.edu/~dg" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2008" doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2008.15" links: doi: "http://doi.ieeecomputersociety.org/10.1109/CSF.2008.15" tags: - "logic" researchr: "https://researchr.org/publication/DeYoungGP08" cites: 0 citedby: 0 pages: "133-145" booktitle: "Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, 23-25 June 2008" publisher: "IEEE Computer Society" isbn: "978-0-7695-3182-3" kind: "inproceedings" key: "DeYoungGP08" - title: "The TPS Theorem Proving System" author: - name: "Peter B. Andrews" link: "https://researchr.org/alias/peter-b.-andrews" - name: "Sunil Issar" link: "https://researchr.org/alias/sunil-issar" - name: "Daniel Nesmith" link: "https://researchr.org/alias/daniel-nesmith" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1988" researchr: "https://researchr.org/publication/AndrewsINP88" cites: 0 citedby: 0 pages: "760-761" booktitle: "9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings" editor: - name: "Ewing L. Lusk" link: "https://researchr.org/alias/ewing-l.-lusk" - name: "Ross A. Overbeek" link: "https://researchr.org/alias/ross-a.-overbeek" volume: "310" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-19343-X" kind: "inproceedings" key: "AndrewsINP88" - title: "A Logical Characterization of Forward and Backward Chaining in the Inverse Method" author: - name: "Kaustuv Chaudhuri" link: "https://researchr.org/alias/kaustuv-chaudhuri" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Greg Price" link: "https://researchr.org/alias/greg-price" year: "2008" doi: "http://dx.doi.org/10.1007/s10817-007-9091-0" links: doi: "http://dx.doi.org/10.1007/s10817-007-9091-0" researchr: "https://researchr.org/publication/ChaudhuriPP08" cites: 0 citedby: 0 journal: "Journal of Automated Reasoning" volume: "40" number: "2-3" pages: "133-177" kind: "article" key: "ChaudhuriPP08" - title: "Structural Cut Elimination" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1995" researchr: "https://researchr.org/publication/Pfenning95" cites: 0 citedby: 0 pages: "156-166" booktitle: "Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, 26-29 June 1995, San Diego, California, USA" publisher: "IEEE Computer Society" kind: "inproceedings" key: "Pfenning95" - title: "Objects as session-typed processes" author: - name: "Stephanie Balzer" link: "https://researchr.org/alias/stephanie-balzer" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2015" doi: "http://doi.acm.org/10.1145/2824815.2824817" links: doi: "http://doi.acm.org/10.1145/2824815.2824817" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/agere/BalzerP15" researchr: "https://researchr.org/publication/BalzerP15" cites: 0 citedby: 0 pages: "13-24" booktitle: "Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE! 2015, Pittsburgh, PA, USA, October 26, 2015" editor: - name: "Elisa Gonzalez Boix" link: "https://researchr.org/alias/elisa-gonzalez-boix" - name: "Philipp Haller" link: "https://researchr.org/alias/philipp-haller" - name: "Alessandro Ricci" link: "https://researchr.org/alias/alessandro-ricci" - name: "Carlos Varela" link: "https://researchr.org/alias/carlos-varela" publisher: "ACM" isbn: "978-1-4503-3901-8" kind: "inproceedings" key: "BalzerP15" - title: "Parallel complexity analysis with temporal session types" author: - name: "Ankush Das" link: "https://researchr.org/alias/ankush-das" - name: "Jan Hoffmann 0002" link: "https://researchr.org/alias/jan-hoffmann-0002" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2018" doi: "https://doi.org/10.1145/3236786" links: doi: "https://doi.org/10.1145/3236786" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/Das0P18" researchr: "https://researchr.org/publication/Das0P18-0" cites: 0 citedby: 0 journal: "Proceedings of the ACM on Programming Languages" volume: "2" number: "ICFP" kind: "article" key: "Das0P18-0" - title: "Uniform Proofs as a Foundation for Logic Programming" author: - name: "Dale Miller" link: "https://researchr.org/alias/dale-miller" - name: "Gopalan Nadathur" link: "https://researchr.org/alias/gopalan-nadathur" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Andre Scedrov" link: "https://researchr.org/alias/andre-scedrov" year: "1991" tags: - "logic programming" - "programming" - "logic" researchr: "https://researchr.org/publication/MillerNPS91" cites: 0 citedby: 0 journal: "Annals of Pure and Applied Logic" volume: "51" number: "1-2" pages: "125-157" kind: "article" key: "MillerNPS91" - title: "Manifest sharing with session types" author: - name: "Stephanie Balzer" link: "https://researchr.org/alias/stephanie-balzer" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2017" doi: "http://doi.acm.org/10.1145/3110281" links: doi: "http://doi.acm.org/10.1145/3110281" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/BalzerP17" researchr: "https://researchr.org/publication/BalzerP17" cites: 0 citedby: 0 journal: "Proceedings of the ACM on Programming Languages" volume: "1" number: "ICFP" kind: "article" key: "BalzerP17" - title: "Compiler Verification in LF" author: - name: "John Hannan" link: "https://researchr.org/alias/john-hannan" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1992" tags: - "compiler" researchr: "https://researchr.org/publication/PfenningH92" cites: 0 citedby: 0 pages: "407-418" booktitle: "Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, 22-25 June 1992, Santa Cruz, California, USA" publisher: "IEEE Computer Society" kind: "inproceedings" key: "PfenningH92" - title: "A Linear Spine Calculus" author: - name: "Iliano Cervesato" link: "https://researchr.org/alias/iliano-cervesato" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" doi: "http://dx.doi.org/10.1093/logcom/13.5.639" links: doi: "http://dx.doi.org/10.1093/logcom/13.5.639" researchr: "https://researchr.org/publication/CervesatoP03" cites: 0 citedby: 0 journal: "Journal of Logic and Computation" volume: "13" number: "5" pages: "639-688" kind: "article" key: "CervesatoP03" - title: "Dependent Types in Practical Programming" author: - name: "Hongwei Xi" link: "http://www.cs.bu.edu/~hwxi/" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1999" doi: "http://doi.acm.org/10.1145/292540.292560" links: doi: "http://doi.acm.org/10.1145/292540.292560" tags: - "programming" researchr: "https://researchr.org/publication/XiP99" cites: 0 citedby: 0 pages: "214-227" booktitle: "POPL" kind: "inproceedings" key: "XiP99" - title: "Unification and Anti-Unification in the Calculus of Constructions" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1991" researchr: "https://researchr.org/publication/Pfenning91" cites: 0 citedby: 0 pages: "74-85" booktitle: "Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, 15-18 July, 1991, Amsterdam, The Netherlands" publisher: "IEEE Computer Society" kind: "inproceedings" key: "Pfenning91" - title: "Types in Logic Programming" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1990" tags: - "logic programming" - "programming" - "logic" researchr: "https://researchr.org/publication/Pfenning90" cites: 0 citedby: 0 pages: "786" booktitle: "ICLP" kind: "inproceedings" key: "Pfenning90" - title: "Note by the Guest Editors" author: - name: "Wilfried Sieg" link: "https://researchr.org/alias/wilfried-sieg" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1998" researchr: "https://researchr.org/publication/SiegP98" cites: 0 citedby: 0 journal: "Studia Logica" volume: "60" number: "1" pages: "1" kind: "article" key: "SiegP98" - title: "Editorial: Strategies in Automated Deduction" author: - name: "Bernhard Gramlich" link: "https://researchr.org/alias/bernhard-gramlich" - name: "Hélène Kirchner" link: "https://researchr.org/alias/h%C3%A9l%C3%A8ne-kirchner" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2000" researchr: "https://researchr.org/publication/GramlichKP00" cites: 0 citedby: 0 journal: "Annals of Mathematics and Artificial Intelligence" volume: "29" number: "1-4" kind: "article" key: "GramlichKP00" - title: "A Universal Session Type for Untyped Asynchronous Communication" author: - name: "Stephanie Balzer" link: "https://researchr.org/alias/stephanie-balzer" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" year: "2018" doi: "https://doi.org/10.4230/LIPIcs.CONCUR.2018.30" links: doi: "https://doi.org/10.4230/LIPIcs.CONCUR.2018.30" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/concur/BalzerPT18" researchr: "https://researchr.org/publication/BalzerPT18" cites: 0 citedby: 0 booktitle: "29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China" editor: - name: "Sven Schewe" link: "https://researchr.org/alias/sven-schewe" - name: "Lijun Zhang 0001" link: "https://researchr.org/alias/lijun-zhang-0001" volume: "118" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-95977-087-3" kind: "inproceedings" key: "BalzerPT18" - title: "A Linear Logic Programming Language for Concurrent Programming over Graph Structures" author: - name: "Flávio Cruz" link: "https://researchr.org/alias/fl%C3%A1vio-cruz" - name: "Ricardo Rocha" link: "https://researchr.org/alias/ricardo-rocha" - name: "Seth Copen Goldstein" link: "https://researchr.org/alias/seth-copen-goldstein" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2014" doi: "http://dx.doi.org/10.1017/S1471068414000167" links: doi: "http://dx.doi.org/10.1017/S1471068414000167" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tplp/CruzRGP14" researchr: "https://researchr.org/publication/CruzRGP14" cites: 0 citedby: 0 journal: "TPLP" volume: "14" number: "4-5" pages: "493-507" kind: "article" key: "CruzRGP14" - title: "Consumable Credentials in Linear-Logic-Based Access-Control Systems" author: - name: "Kevin D. Bowers" link: "https://researchr.org/alias/kevin-d.-bowers" - name: "Lujo Bauer" link: "https://researchr.org/alias/lujo-bauer" - name: "Deepak Garg" link: "http://www.cs.cmu.edu/~dg" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Michael K. Reiter" link: "https://researchr.org/alias/michael-k.-reiter" year: "2007" doi: "http://www.isoc.org/isoc/conferences/ndss/07/papers/consumable_credentials.pdf" links: doi: "http://www.isoc.org/isoc/conferences/ndss/07/papers/consumable_credentials.pdf" tags: - "control systems" - "rule-based" - "logic" - "access control" - "role-based access control" researchr: "https://researchr.org/publication/BowersBGPR07" cites: 0 citedby: 0 booktitle: "Proceedings of the Network and Distributed System Security Symposium, NDSS 2007, San Diego, California, USA, 28th February - 2nd March 2007" publisher: "The Internet Society" kind: "inproceedings" key: "BowersBGPR07" - title: "Polarized Substructural Session Types" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Dennis Griffith" link: "https://researchr.org/alias/dennis-griffith" year: "2015" doi: "http://dx.doi.org/10.1007/978-3-662-46678-0_1" links: doi: "http://dx.doi.org/10.1007/978-3-662-46678-0_1" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fossacs/PfenningG15" researchr: "https://researchr.org/publication/PfenningG15" cites: 0 citedby: 0 pages: "3-22" booktitle: "Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings" editor: - name: "Andrew M. Pitts" link: "https://researchr.org/alias/andrew-m.-pitts" volume: "9034" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-662-46677-3" kind: "inproceedings" key: "PfenningG15" - title: "On proving syntactic properties of CPS programs" author: - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" - name: "Belmina Dzafic" link: "https://researchr.org/alias/belmina-dzafic" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1999" doi: "http://www.elsevier.com/gej-ng/31/29/23/50/23/show/Products/notes/index.htt#003" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/50/23/show/Products/notes/index.htt#003" researchr: "https://researchr.org/publication/DanvyDP99" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "26" pages: "21-33" kind: "article" key: "DanvyDP99" - title: "Programming with Higher-Order Logic, by Dale Miller and Gopalan Nadathur, Cambridge University Press, 2012, Hardcover, ISBN-10: 052187940X, xiv + 306 pp" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2014" doi: "http://dx.doi.org/10.1017/S1471068414000027" links: doi: "http://dx.doi.org/10.1017/S1471068414000027" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tplp/Pfenning14" researchr: "https://researchr.org/publication/Pfenning14" cites: 0 citedby: 0 journal: "TPLP" volume: "14" number: "2" pages: "265-267" kind: "article" key: "Pfenning14" - title: "On a Logical Foundation for Explicit Substitutions" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2007" doi: "http://dx.doi.org/10.1007/978-3-540-73449-9_3" links: doi: "http://dx.doi.org/10.1007/978-3-540-73449-9_3" researchr: "https://researchr.org/publication/Pfenning07" cites: 0 citedby: 0 pages: "19" booktitle: "Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings" editor: - name: "Franz Baader" link: "https://researchr.org/alias/franz-baader" volume: "4533" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-73447-5" kind: "inproceedings" key: "Pfenning07" - title: "Unification via Explicit Substitutions: The Case of Higher-Order Patterns" author: - name: "Gilles Dowek" link: "https://researchr.org/alias/gilles-dowek" - name: "Thérèse Hardin" link: "https://researchr.org/alias/th%C3%A9r%C3%A8se-hardin" - name: "Claude Kirchner" link: "https://researchr.org/alias/claude-kirchner" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1996" researchr: "https://researchr.org/publication/DowekHKP96" cites: 0 citedby: 0 pages: "259-273" booktitle: "JICSLP" kind: "inproceedings" key: "DowekHKP96" - title: "Structural Cut Elimination: I. Intuitionistic and Classical Logic" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2000" tags: - "logic" researchr: "https://researchr.org/publication/Pfenning00%3A0" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "157" number: "1-2" pages: "84-141" kind: "article" key: "Pfenning00:0" - title: "A type theory for memory allocation and data layout" author: - name: "Leaf Petersen" link: "https://researchr.org/alias/leaf-petersen" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" doi: "http://doi.acm.org/10.1145/640128.604147" links: doi: "http://doi.acm.org/10.1145/640128.604147" tags: - "layout" - "data-flow" - "type theory" researchr: "https://researchr.org/publication/PetersenHCP03" cites: 0 citedby: 0 pages: "172-184" booktitle: "POPL" kind: "inproceedings" key: "PetersenHCP03" - title: "Towards concurrent type theory" author: - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" year: "2012" doi: "http://doi.acm.org/10.1145/2103786.2103788" links: doi: "http://doi.acm.org/10.1145/2103786.2103788" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/tldi/CairesPT12" researchr: "https://researchr.org/publication/CairesPT12" cites: 0 citedby: 0 pages: "1-12" booktitle: "Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012" editor: - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "ACM" isbn: "978-1-4503-1120-5" kind: "inproceedings" key: "CairesPT12" - title: "Monitors and blame assignment for higher-order session types" author: - name: "Limin Jia" link: "https://researchr.org/alias/limin-jia" - name: "Hannah Gommerstadt" link: "https://researchr.org/alias/hannah-gommerstadt" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2016" doi: "http://doi.acm.org/10.1145/2837614.2837662" links: doi: "http://doi.acm.org/10.1145/2837614.2837662" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/JiaGP16" researchr: "https://researchr.org/publication/JiaGP16" cites: 0 citedby: 0 pages: "582-594" booktitle: "Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016" editor: - name: "Rastislav Bodik" link: "https://researchr.org/alias/rastislav-bodik" - name: "Rupak Majumdar" link: "https://researchr.org/alias/rupak-majumdar" publisher: "ACM" isbn: "978-1-4503-3549-2" kind: "inproceedings" key: "JiaGP16" - title: "Functions as Session-Typed Processes" author: - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2012" doi: "http://dx.doi.org/10.1007/978-3-642-28729-9_23" links: doi: "http://dx.doi.org/10.1007/978-3-642-28729-9_23" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fossacs/ToninhoCP12" researchr: "https://researchr.org/publication/ToninhoCP12" cites: 0 citedby: 0 pages: "346-360" booktitle: "Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings" editor: - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" volume: "7213" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-28728-2" kind: "inproceedings" key: "ToninhoCP12" - title: "A Concurrent Logical Framework: The Propositional Fragment" author: - name: "Kevin Watkins" link: "https://researchr.org/alias/kevin-watkins" - name: "Iliano Cervesato" link: "https://researchr.org/alias/iliano-cervesato" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "David Walker" link: "https://researchr.org/alias/david-walker" year: "2003" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3085&spage=355" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3085&spage=355" researchr: "https://researchr.org/publication/WatkinsCPW03" cites: 0 citedby: 0 pages: "355-377" booktitle: "Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers" editor: - name: "Stefano Berardi" link: "https://researchr.org/alias/stefano-berardi" - name: "Mario Coppo" link: "https://researchr.org/alias/mario-coppo" - name: "Ferruccio Damiani" link: "https://researchr.org/alias/ferruccio-damiani" volume: "3085" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-22164-6" kind: "inproceedings" key: "WatkinsCPW03" - title: "Primitive Recursion for Higher-Order Abstract Syntax" author: - name: "Joëlle Despeyroux" link: "https://researchr.org/alias/jo%C3%ABlle-despeyroux" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Carsten Schürmann" link: "https://researchr.org/alias/carsten-sch%C3%BCrmann" year: "1997" tags: - "abstract syntax" researchr: "https://researchr.org/publication/DespeyrouxPS97" cites: 0 citedby: 0 pages: "147-163" booktitle: "Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA 97, Nancy, France, April 2-4, 1997, Proceedings" editor: - name: "Philippe de Groote" link: "https://researchr.org/alias/philippe-de-groote" volume: "1210" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-62688-3" kind: "inproceedings" key: "DespeyrouxPS97" - title: "Trustless Grid Computing in ConCert" author: - name: "Bor-Yuh Evan Chang" link: "https://researchr.org/alias/bor-yuh-evan-chang" - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Margaret DeLap" link: "https://researchr.org/alias/margaret-delap" - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Jason Liszka" link: "https://researchr.org/alias/jason-liszka" - name: "Tom Murphy VII" link: "https://researchr.org/alias/tom-murphy-vii" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2002" doi: "http://link.springer.de/link/service/series/0558/bibs/2536/25360112.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2536/25360112.htm" researchr: "https://researchr.org/publication/ChangCDHLVP02" cites: 0 citedby: 0 pages: "112-125" booktitle: "Grid Computing - GRID 2002, Third International Workshop, Baltimore, MD, USA, November 18, 2002, Proceedings" editor: - name: "Manish Parashar" link: "https://researchr.org/alias/manish-parashar" volume: "2536" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-00133-6" kind: "inproceedings" key: "ChangCDHLVP02" - title: "Editorial" author: - name: "Martín Abadi" link: "https://researchr.org/alias/mart%C3%ADn-abadi" - name: "Leonid Libkin" link: "https://researchr.org/alias/leonid-libkin" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2002" doi: "http://doi.acm.org/10.1145/507382.507383" links: doi: "http://doi.acm.org/10.1145/507382.507383" researchr: "https://researchr.org/publication/AbadiLP02" cites: 0 citedby: 0 journal: "ACM Trans. Comput. Log." volume: "3" number: "3" pages: "335" kind: "article" key: "AbadiLP02" - title: "Tridirectional typechecking" author: - name: "Joshua Dunfield" link: "https://researchr.org/alias/joshua-dunfield" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2004" doi: "http://doi.acm.org/10.1145/964001.964025" links: doi: "http://doi.acm.org/10.1145/964001.964025" researchr: "https://researchr.org/publication/DunfieldP04" cites: 0 citedby: 0 pages: "281-292" 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: "DunfieldP04" - title: "A Logical Characterization of Forward and Backward Chaining in the Inverse Method" author: - name: "Kaustuv Chaudhuri" link: "https://researchr.org/alias/kaustuv-chaudhuri" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Greg Price" link: "https://researchr.org/alias/greg-price" year: "2006" doi: "http://dx.doi.org/10.1007/11814771_9" links: doi: "http://dx.doi.org/10.1007/11814771_9" researchr: "https://researchr.org/publication/ChaudhuriPP06" cites: 0 citedby: 0 pages: "97-111" booktitle: "Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings" editor: - name: "Ulrich Furbach" link: "https://researchr.org/alias/ulrich-furbach" - name: "Natarajan Shankar" link: "https://researchr.org/alias/natarajan-shankar" volume: "4130" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-37187-7" kind: "inproceedings" key: "ChaudhuriPP06" - title: "A modal analysis of staged computation" author: - name: "Rowan Davies" link: "https://researchr.org/alias/rowan-davies" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2001" doi: "http://doi.acm.org/10.1145/382780.382785" links: doi: "http://doi.acm.org/10.1145/382780.382785" tags: - "analysis" - "staged computation" researchr: "https://researchr.org/publication/DaviesP01" cites: 0 citedby: 0 journal: "Journal of the ACM" volume: "48" number: "3" pages: "555-604" kind: "article" key: "DaviesP01" - title: "Verifying Uniqueness in a Logical Framework" author: - name: "Penny Anderson" link: "https://researchr.org/alias/penny-anderson" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2004" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3223&spage=18" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3223&spage=18" researchr: "https://researchr.org/publication/AndersonP04%3A0" cites: 0 citedby: 0 pages: "18-33" booktitle: "Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings" editor: - name: "Konrad Slind" link: "https://researchr.org/alias/konrad-slind" - name: "Annette Bunker" link: "https://researchr.org/alias/annette-bunker" - name: "Ganesh Gopalakrishnan" link: "https://researchr.org/alias/ganesh-gopalakrishnan" volume: "3223" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-23017-3" kind: "inproceedings" key: "AndersonP04:0" - title: "Elf: A Meta-Language for Deductive Systems (System Descrition)" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1994" tags: - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/Pfenning94" cites: 0 citedby: 0 pages: "811-815" booktitle: "Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings" editor: - name: "Alan Bundy" link: "https://researchr.org/alias/alan-bundy" volume: "814" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-58156-1" kind: "inproceedings" key: "Pfenning94" - title: "The Type System of a Higher-Order Logic Programming Language" author: - name: "Gopalan Nadathur" link: "https://researchr.org/alias/gopalan-nadathur" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1992" tags: - "programming languages" - "type system" - "logic programming" - "programming" - "logic" researchr: "https://researchr.org/publication/NadathurP92" cites: 0 citedby: 0 pages: "245-283" booktitle: "Types in Logic Programming" kind: "incollection" key: "NadathurP92" - title: "On the Logical Foundations of Staged Computation (Abstract of Invited Talk)" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2000" doi: "http://doi.acm.org/10.1145/328690.328696" links: doi: "http://doi.acm.org/10.1145/328690.328696" tags: - "staged computation" researchr: "https://researchr.org/publication/Pfenning00%3A1" cites: 0 citedby: 0 pages: "33" booktitle: "PEPM" kind: "inproceedings" key: "Pfenning00:1" - title: "Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk)" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2004" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3302&spage=196" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3302&spage=196" tags: - "semantics" - "operational semantics" researchr: "https://researchr.org/publication/Pfenning04" cites: 0 citedby: 0 pages: "196" booktitle: "Programming Languages and Systems: Second Asian Symposium, APLAS 2004, Taipei, Taiwan, November 4-6, 2004. Proceedings" editor: - name: "Wei-Ngan Chin" link: "https://researchr.org/alias/wei-ngan-chin" volume: "3302" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-23724-0" kind: "inproceedings" key: "Pfenning04" - title: "Type Assignment for Intersections and Unions in Call-by-Value Languages" author: - name: "Joshua Dunfield" link: "https://researchr.org/alias/joshua-dunfield" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" doi: "http://link.springer.de/link/service/series/0558/bibs/2620/26200250.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2620/26200250.htm" researchr: "https://researchr.org/publication/DunfieldP03" cites: 0 citedby: 0 pages: "250-266" booktitle: "Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings" editor: - name: "Andrew D. Gordon" link: "http://research.microsoft.com/en-us/um/people/adg/" volume: "2620" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-00897-7" kind: "inproceedings" key: "DunfieldP03" - title: "Subtyping and intersection types revisited" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2007" doi: "http://doi.acm.org/10.1145/1291151.1291153" links: doi: "http://doi.acm.org/10.1145/1291151.1291153" tags: - "subtyping" researchr: "https://researchr.org/publication/Pfenning07%3A0" cites: 0 citedby: 0 pages: "219" booktitle: "Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007" editor: - name: "Ralf Hinze" link: "https://researchr.org/alias/ralf-hinze" - name: "Norman Ramsey" link: "http://www.cs.tufts.edu/~nr/" publisher: "ACM" isbn: "978-1-59593-815-2" kind: "inproceedings" key: "Pfenning07:0" - title: "The Ergo Attribute System" author: - name: "Robert L. Nord" link: "https://researchr.org/alias/robert-l.-nord" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1988" researchr: "https://researchr.org/publication/NordP88" cites: 0 citedby: 0 pages: "110-120" booktitle: "Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments" address: "New York, USA" publisher: "ACM" kind: "inproceedings" key: "NordP88" - title: "Partial Polymorphic Type Inference and Higher-Order Unification" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1988" doi: "http://doi.acm.org/10.1145/62678.62697" links: doi: "http://doi.acm.org/10.1145/62678.62697" tags: - "type inference" researchr: "https://researchr.org/publication/Pfenning88%3A0" cites: 0 citedby: 0 pages: "153-163" booktitle: "LISP and Functional Programming" kind: "inproceedings" key: "Pfenning88:0" - title: "A modal foundation for meta-variables" author: - name: "Aleksandar Nanevski" link: "https://researchr.org/alias/aleksandar-nanevski" - name: "Brigitte Pientka" link: "https://researchr.org/alias/brigitte-pientka" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2003" doi: "http://doi.acm.org/10.1145/976571.976582" links: doi: "http://doi.acm.org/10.1145/976571.976582" tags: - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/NanevskiPP03" cites: 0 citedby: 0 booktitle: "Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003" publisher: "ACM" kind: "inproceedings" key: "NanevskiPP03" - title: "Unification in a Lambda-Calculus with Intersection Types" author: - name: "Michael Kohlhase" link: "https://researchr.org/alias/michael-kohlhase" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1993" researchr: "https://researchr.org/publication/KohlhaseP93" cites: 0 citedby: 0 pages: "488-505" booktitle: "ILPS" kind: "inproceedings" key: "KohlhaseP93" - title: "A Learning Algorithm for Localizing People Based on Wireless Signal Strength that Uses Labeled and Unlabeled Data" author: - name: "Sebastian Thrun" link: "https://researchr.org/alias/sebastian-thrun" - name: "Geoffrey J. Gordon" link: "https://researchr.org/alias/geoffrey-j.-gordon" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Mary Berna" link: "https://researchr.org/alias/mary-berna" - name: "Brennan Sellner" link: "https://researchr.org/alias/brennan-sellner" - name: "Brad Lisien" link: "https://researchr.org/alias/brad-lisien" year: "2003" tags: - "rule-based" researchr: "https://researchr.org/publication/ThrunGPBSL03" cites: 0 citedby: 0 pages: "1427-1428" booktitle: "IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003" editor: - name: "Georg Gottlob" link: "https://researchr.org/alias/georg-gottlob" - name: "Toby Walsh" link: "https://researchr.org/alias/toby-walsh" publisher: "Morgan Kaufmann" kind: "inproceedings" key: "ThrunGPBSL03" - title: "Refinement Types for ML" author: - name: "Tim Freeman" link: "https://researchr.org/alias/tim-freeman" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1991" tags: - "refinement" researchr: "https://researchr.org/publication/FreemanP91" cites: 0 citedby: 0 pages: "268-277" booktitle: "PLDI" kind: "inproceedings" key: "FreemanP91" - title: "Primitive recursion for higher-order abstract syntax" author: - name: "Carsten Schürmann" link: "https://researchr.org/alias/carsten-sch%C3%BCrmann" - name: "Joëlle Despeyroux" link: "https://researchr.org/alias/jo%C3%ABlle-despeyroux" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2001" doi: "http://dx.doi.org/10.1016/S0304-3975(00)00418-7" links: doi: "http://dx.doi.org/10.1016/S0304-3975(00)00418-7" tags: - "abstract syntax" researchr: "https://researchr.org/publication/SchurmannDP01" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "266" number: "1-2" pages: "1-57" kind: "article" key: "SchurmannDP01" - title: "Contextual modal type theory" author: - name: "Aleksandar Nanevski" link: "https://researchr.org/alias/aleksandar-nanevski" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Brigitte Pientka" link: "https://researchr.org/alias/brigitte-pientka" year: "2008" doi: "http://doi.acm.org/10.1145/1352582.1352591" links: doi: "http://doi.acm.org/10.1145/1352582.1352591" tags: - "type theory" researchr: "https://researchr.org/publication/NanevskiPP08" cites: 0 citedby: 0 journal: "ACM Trans. Comput. Log." volume: "9" number: "3" kind: "article" key: "NanevskiPP08" - title: "Higher-Order Processes, Functions, and Sessions: A Monadic Integration" author: - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-642-37036-6_20" links: doi: "http://dx.doi.org/10.1007/978-3-642-37036-6_20" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/ToninhoCP13" researchr: "https://researchr.org/publication/ToninhoCP13" cites: 0 citedby: 0 pages: "350-369" booktitle: "Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings" editor: - name: "Matthias Felleisen" link: "http://www.ccs.neu.edu/home/matthias/" - name: "Philippa Gardner" link: "https://researchr.org/alias/philippa-gardner" volume: "7792" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-37035-9" kind: "inproceedings" key: "ToninhoCP13" - title: "Algorithms for Equality and Unification in the Presence of Notational Definitions" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Carsten Schürmann" link: "https://researchr.org/alias/carsten-sch%C3%BCrmann" year: "1998" doi: "http://link.springer.de/link/service/series/0558/bibs/1657/16570179.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1657/16570179.htm" researchr: "https://researchr.org/publication/PfenningS98%3A0" cites: 0 citedby: 0 pages: "179-193" booktitle: "Types for Proofs and Programs, International Workshop TYPES 98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers" editor: - name: "Thorsten Altenkirch" link: "http://www.cs.nott.ac.uk/~txa" - name: "Wolfgang Naraschewski" link: "https://researchr.org/alias/wolfgang-naraschewski" - name: "Bernhard Reus" link: "https://researchr.org/alias/bernhard-reus" volume: "1657" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-66537-4" kind: "inproceedings" key: "PfenningS98:0" - title: "Algorithms for Equality and Unification in the Presence of Notational Definitions" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Carsten Schürmann" link: "https://researchr.org/alias/carsten-sch%C3%BCrmann" year: "1998" doi: "http://www.elsevier.com/gej-ng/31/29/23/41/23/show/Products/notes/index.htt#006" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/41/23/show/Products/notes/index.htt#006" researchr: "https://researchr.org/publication/PfenningS98" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "17" pages: "1-13" kind: "article" key: "PfenningS98" - title: "Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication" author: - name: "Henry DeYoung" link: "https://researchr.org/alias/henry-deyoung" - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" year: "2012" doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2012.228" links: doi: "http://dx.doi.org/10.4230/LIPIcs.CSL.2012.228" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/DeYoungCPT12" researchr: "https://researchr.org/publication/DeYoungCPT12" cites: 0 citedby: 0 pages: "228-242" booktitle: "Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France" editor: - name: "Patrick Cégielski" link: "https://researchr.org/alias/patrick-c%C3%A9gielski" - name: "Arnaud Durand" link: "https://researchr.org/alias/arnaud-durand" volume: "16" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik" isbn: "978-3-939897-42-2" kind: "inproceedings" key: "DeYoungCPT12" - title: "Substructural Proofs as Automata" author: - name: "Henry DeYoung" link: "https://researchr.org/alias/henry-deyoung" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2016" doi: "http://dx.doi.org/10.1007/978-3-319-47958-3_1" links: doi: "http://dx.doi.org/10.1007/978-3-319-47958-3_1" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/aplas/DeYoungP16" researchr: "https://researchr.org/publication/DeYoungP16" cites: 0 citedby: 0 pages: "3-22" booktitle: "Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings" editor: - name: "Atsushi Igarashi" link: "https://researchr.org/alias/atsushi-igarashi" volume: "10017" series: "Lecture Notes in Computer Science" isbn: "978-3-319-47957-6" kind: "inproceedings" key: "DeYoungP16" - title: "Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method" author: - name: "Sean McLaughlin" link: "https://researchr.org/alias/sean-mclaughlin" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2009" doi: "http://dx.doi.org/10.1007/978-3-642-02959-2_19" links: doi: "http://dx.doi.org/10.1007/978-3-642-02959-2_19" researchr: "https://researchr.org/publication/McLaughlinP09" cites: 0 citedby: 0 pages: "230-244" booktitle: "Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings" editor: - name: "Renate A. Schmidt" link: "https://researchr.org/alias/renate-a.-schmidt" volume: "5663" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-02958-5" kind: "inproceedings" key: "McLaughlinP09" - title: "Intuitionistic Letcc via Labelled Deduction" author: - name: "Jason Reed" link: "https://researchr.org/alias/jason-reed" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2009" doi: "http://dx.doi.org/10.1016/j.entcs.2009.02.031" links: doi: "http://dx.doi.org/10.1016/j.entcs.2009.02.031" researchr: "https://researchr.org/publication/ReedP09" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "231" pages: "91-111" kind: "article" key: "ReedP09" - title: "A Proof-Carrying File System" author: - name: "Deepak Garg" link: "https://researchr.org/alias/deepak-garg" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2010" doi: "http://doi.ieeecomputersociety.org/10.1109/SP.2010.28" links: doi: "http://doi.ieeecomputersociety.org/10.1109/SP.2010.28" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sp/GargP10" researchr: "https://researchr.org/publication/GargP10" cites: 0 citedby: 0 pages: "349-364" booktitle: "31st IEEE Symposium on Security and Privacy, S&P 2010, 16-19 May 2010, Berleley/Oakland, California, USA" publisher: "IEEE Computer Society" isbn: "978-0-7695-4035-1" kind: "inproceedings" key: "GargP10" - title: "Staged computation with names and necessity" author: - name: "Aleksandar Nanevski" link: "https://researchr.org/alias/aleksandar-nanevski" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2005" doi: "http://dx.doi.org/10.1017/S095679680500568X" links: doi: "http://dx.doi.org/10.1017/S095679680500568X" tags: - "staged computation" researchr: "https://researchr.org/publication/NanevskiP05" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "15" number: "5" pages: "893-939" kind: "article" key: "NanevskiP05" - title: "Presenting Intuitive Deductions via Symmetric Simplification" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Dan Nesmith" link: "https://researchr.org/alias/dan-nesmith" year: "1990" researchr: "https://researchr.org/publication/PfenningN90" cites: 0 citedby: 0 pages: "336-350" booktitle: "10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings" editor: - name: "Mark E. Stickel" link: "https://researchr.org/alias/mark-e.-stickel" volume: "449" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-52885-7" kind: "inproceedings" key: "PfenningN90" - title: "On equivalence and canonical forms in the LF type theory" author: - name: "Robert Harper" link: "http://www.cs.cmu.edu/~rwh/" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2005" doi: "http://doi.acm.org/10.1145/1042038.1042041" links: doi: "http://doi.acm.org/10.1145/1042038.1042041" tags: - "type theory" researchr: "https://researchr.org/publication/HarperP05" cites: 0 citedby: 0 journal: "ACM Trans. Comput. Log." volume: "6" number: "1" pages: "61-101" kind: "article" key: "HarperP05" - title: "Higher-Order Logic Programming as Constraint Logic Programming" author: - name: "Spiro Michaylov" link: "https://researchr.org/alias/spiro-michaylov" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1993" tags: - "constraints" - "logic programming" - "programming" - "logic" researchr: "https://researchr.org/publication/MichaylovP93" cites: 0 citedby: 0 pages: "210-218" booktitle: "PPCP" kind: "inproceedings" key: "MichaylovP93" - title: "A Linear Logical Framework" author: - name: "Iliano Cervesato" link: "https://researchr.org/alias/iliano-cervesato" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2002" doi: "http://dx.doi.org/10.1006/inco.2001.2951" links: doi: "http://dx.doi.org/10.1006/inco.2001.2951" researchr: "https://researchr.org/publication/CervesatoP02" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "179" number: "1" pages: "19-75" kind: "article" key: "CervesatoP02" - title: "Modal Types as Staging Specifications for Run-Time Code Generation" author: - name: "Philip Wickline" link: "https://researchr.org/alias/philip-wickline" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Rowan Davies" link: "https://researchr.org/alias/rowan-davies" year: "1998" doi: "http://doi.acm.org/10.1145/289121.289129" links: doi: "http://doi.acm.org/10.1145/289121.289129" tags: - "code generation" researchr: "https://researchr.org/publication/WicklineLPD98" cites: 0 citedby: 0 journal: "ACM Computing Surveys" volume: "30" number: "3es" pages: "8" kind: "article" key: "WicklineLPD98" - title: "Run-time Code Generation and Modal-ML" author: - name: "Philip Wickline" link: "https://researchr.org/alias/philip-wickline" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1998" tags: - "code generation" researchr: "https://researchr.org/publication/WicklineLP98" cites: 0 citedby: 0 pages: "224-235" booktitle: "PLDI" kind: "inproceedings" key: "WicklineLP98" - title: "Specifying Properties of Concurrent Computations in CLF" author: - name: "Kevin Watkins" link: "https://researchr.org/alias/kevin-watkins" - name: "Iliano Cervesato" link: "https://researchr.org/alias/iliano-cervesato" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "David Walker" link: "https://researchr.org/alias/david-walker" year: "2008" doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.013" links: doi: "http://dx.doi.org/10.1016/j.entcs.2007.11.013" researchr: "https://researchr.org/publication/WatkinsCPW08" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "199" pages: "67-87" kind: "article" key: "WatkinsCPW08" - title: "Preface" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2002" doi: "http://www.elsevier.com/gej-ng/31/29/23/125/50/show/Products/notes/index.htt#001" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/125/50/show/Products/notes/index.htt#001" researchr: "https://researchr.org/publication/Pfenning02" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "70" number: "2" pages: "146" kind: "article" key: "Pfenning02" - title: "Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic" author: - name: "J. Polokow" link: "https://researchr.org/alias/j.-polokow" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1999" doi: "http://www.elsevier.com/gej-ng/31/29/23/44/23/show/Products/notes/index.htt#026" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/44/23/show/Products/notes/index.htt#026" tags: - "logic" researchr: "https://researchr.org/publication/PolokowP99" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "20" pages: "449-466" kind: "article" key: "PolokowP99" - title: "On a Logical Foundation for Explicit Substitutions" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2007" doi: "http://dx.doi.org/10.1007/978-3-540-73228-0_1" links: doi: "http://dx.doi.org/10.1007/978-3-540-73228-0_1" researchr: "https://researchr.org/publication/Pfenning07%3A1" cites: 0 citedby: 0 pages: "1" booktitle: "Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings" editor: - name: "Simona Ronchi Della Rocca" link: "http://www.di.unito.it/~ronchi/" volume: "4583" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-73227-3" kind: "inproceedings" key: "Pfenning07:1" - title: "Proof-Carrying Code in a Session-Typed Process Calculus" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" year: "2011" doi: "http://dx.doi.org/10.1007/978-3-642-25379-9_4" links: doi: "http://dx.doi.org/10.1007/978-3-642-25379-9_4" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/PfenningCT11" researchr: "https://researchr.org/publication/PfenningCT11" cites: 0 citedby: 0 pages: "21-36" booktitle: "Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings" editor: - name: "Jean-Pierre Jouannaud" link: "https://researchr.org/alias/jean-pierre-jouannaud" - name: "Zhong Shao" link: "https://researchr.org/alias/zhong-shao" volume: "7086" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-25378-2" kind: "inproceedings" key: "PfenningCT11" - title: "Inductively Defined Types in the Calculus of Constructions" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Christine Paulin-Mohring" link: "https://researchr.org/alias/christine-paulin-mohring" year: "1989" researchr: "https://researchr.org/publication/PfenningP89" cites: 0 citedby: 0 pages: "209-228" booktitle: "Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29 - April 1, 1989, Proceedings" editor: - name: "Michael G. Main" link: "https://researchr.org/alias/michael-g.-main" - name: "Austin Melton" link: "https://researchr.org/alias/austin-melton" - name: "Michael W. Mislove" link: "https://researchr.org/alias/michael-w.-mislove" - name: "David A. Schmidt" link: "https://researchr.org/alias/david-a.-schmidt" volume: "442" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-97375-3" kind: "inproceedings" key: "PfenningP89" - title: "Efficient Resource Management for Linear Logic Proof Search" author: - name: "Iliano Cervesato" link: "https://researchr.org/alias/iliano-cervesato" - name: "Joshua S. Hodas" link: "https://researchr.org/alias/joshua-s.-hodas" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1996" tags: - "logic" - "search" researchr: "https://researchr.org/publication/CervesatoHP96" cites: 0 citedby: 0 pages: "67-81" booktitle: "Extensions of Logic Programming, 5th International Workshop, ELP 96, Leipzig, Germany, March 28-30, 1996, Proceedings" editor: - name: "Roy Dyckhoff" link: "https://researchr.org/alias/roy-dyckhoff" - name: "Heinrich Herre" link: "https://researchr.org/alias/heinrich-herre" - name: "Peter Schroeder-Heister" link: "https://researchr.org/alias/peter-schroeder-heister" volume: "1050" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-60983-0" kind: "inproceedings" key: "CervesatoHP96" - title: "Invited talk: Tri-Directional Type Checking" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2002" doi: "http://www1.elsevier.com/gej-ng/31/29/23/125/51/show/Products/notes/index.htt#012" links: doi: "http://www1.elsevier.com/gej-ng/31/29/23/125/51/show/Products/notes/index.htt#012" tags: - "type checking" researchr: "https://researchr.org/publication/Pfenning02a" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "70" number: "1" kind: "article" key: "Pfenning02a" - title: "Implementing the Meta-Theory of Deductive Systems" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Ekkehard Rohwedder" link: "https://researchr.org/alias/ekkehard-rohwedder" year: "1992" tags: - "meta-model" - "Meta-Environment" - "meta-objects" researchr: "https://researchr.org/publication/PfenningR92" cites: 0 citedby: 0 pages: "537-551" booktitle: "Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings" editor: - name: "Deepak Kapur" link: "https://researchr.org/alias/deepak-kapur" volume: "607" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-55602-8" kind: "inproceedings" key: "PfenningR92" - title: "Natural Deduction for Intuitionistic Non-communicative Linear Logic" author: - name: "Jeff Polakow" link: "https://researchr.org/alias/jeff-polakow" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1999" doi: "http://link.springer.de/link/service/series/0558/bibs/1581/15810295.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/1581/15810295.htm" tags: - "logic" researchr: "https://researchr.org/publication/PolakowP99" cites: 0 citedby: 0 pages: "295-309" booktitle: "Typed Lambda Calculi and Applications, 4th International Conference, TLCA 99, L Aquila, Italy, April 7-9, 1999, Proceedings" editor: - name: "Jean-Yves Girard" link: "https://researchr.org/alias/jean-yves-girard" volume: "1581" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-65763-0" kind: "inproceedings" key: "PolakowP99" - title: "The TPS Theorem Proving System" author: - name: "Peter B. Andrews" link: "https://researchr.org/alias/peter-b.-andrews" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Sunil Issar" link: "https://researchr.org/alias/sunil-issar" - name: "C. P. Klapper" link: "https://researchr.org/alias/c.-p.-klapper" year: "1986" tags: - "C++" researchr: "https://researchr.org/publication/AndrewsPIK86" cites: 0 citedby: 0 pages: "663-664" booktitle: "8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings" editor: - name: "Jörg H. Siekmann" link: "https://researchr.org/alias/j%C3%B6rg-h.-siekmann" volume: "230" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-16780-3" kind: "inproceedings" key: "AndrewsPIK86" - title: "Work Analysis with Resource-Aware Session Types" author: - name: "Ankush Das" link: "https://researchr.org/alias/ankush-das" - name: "Jan Hoffmann 0002" link: "https://researchr.org/alias/jan-hoffmann-0002" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2018" doi: "http://doi.acm.org/10.1145/3209108.3209146" links: doi: "http://doi.acm.org/10.1145/3209108.3209146" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/Das0P18" researchr: "https://researchr.org/publication/Das0P18" cites: 0 citedby: 0 pages: "305-314" booktitle: "Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018" editor: - name: "Anuj Dawar" link: "https://researchr.org/alias/anuj-dawar" - name: "Erich Grädel" link: "https://researchr.org/alias/erich-gr%C3%A4del" publisher: "ACM" kind: "inproceedings" key: "Das0P18" - title: "Eliminating Array Bound Checking Through Dependent Types" author: - name: "Hongwei Xi" link: "http://www.cs.bu.edu/~hwxi/" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1998" tags: - "type checking" researchr: "https://researchr.org/publication/XiP98" cites: 0 citedby: 0 pages: "249-257" booktitle: "PLDI" kind: "inproceedings" key: "XiP98" - title: "Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization" author: - name: "Scott Dietzen" link: "https://researchr.org/alias/scott-dietzen" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1989" tags: - "rule-based" - "modal logic" - "logic" researchr: "https://researchr.org/publication/DietzenP89" cites: 0 citedby: 0 pages: "447-449" booktitle: "Proceedings of the Sixth International Workshop on Machine Learning (ML 1989), Cornell University, Ithaca, New York, USA, June 26-27, 1989" editor: - name: "Alberto Maria Segre" link: "https://researchr.org/alias/alberto-maria-segre" publisher: "Morgan Kaufmann" isbn: "1-55860-036-1" kind: "inproceedings" key: "DietzenP89" - title: "Monadic concurrent linear logic programming" author: - name: "Pablo López" link: "https://researchr.org/alias/pablo-l%C3%B3pez" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Jeff Polakow" link: "https://researchr.org/alias/jeff-polakow" - name: "Kevin Watkins" link: "https://researchr.org/alias/kevin-watkins" year: "2005" doi: "http://doi.acm.org/10.1145/1069774.1069778" links: doi: "http://doi.acm.org/10.1145/1069774.1069778" tags: - "logic programming" - "programming" - "logic" researchr: "https://researchr.org/publication/LopezPPW05" cites: 0 citedby: 0 pages: "35-46" booktitle: "Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 11-13 2005, Lisbon, Portugal" editor: - name: "Pedro Barahona" link: "https://researchr.org/alias/pedro-barahona" - name: "Amy P. Felty" link: "https://researchr.org/alias/amy-p.-felty" publisher: "ACM" isbn: "1-59593-090-6" kind: "inproceedings" key: "LopezPPW05" - title: "Linear logic propositions as session types" author: - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" year: "2016" doi: "http://dx.doi.org/10.1017/S0960129514000218" links: doi: "http://dx.doi.org/10.1017/S0960129514000218" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/mscs/CairesPT16" researchr: "https://researchr.org/publication/CairesPT16" cites: 0 citedby: 0 journal: "Mathematical Structures in Computer Science" volume: "26" number: "3" pages: "367-423" kind: "article" key: "CairesPT16" - title: "Dependent session types via intuitionistic linear type theory" author: - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2011" doi: "http://doi.acm.org/10.1145/2003476.2003499" links: doi: "http://doi.acm.org/10.1145/2003476.2003499" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/ToninhoCP11" researchr: "https://researchr.org/publication/ToninhoCP11" cites: 0 citedby: 0 pages: "161-172" booktitle: "Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20-22, 2011, Odense, Denmark" editor: - name: "Peter Schneider-Kamp" link: "https://researchr.org/alias/peter-schneider-kamp" - name: "Michael Hanus" link: "https://researchr.org/alias/michael-hanus" publisher: "ACM" isbn: "978-1-4503-0776-5" kind: "inproceedings" key: "ToninhoCP11" - title: "On a modal lambda calculus for S4" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Hao Chi Wong" link: "https://researchr.org/alias/hao-chi-wong" year: "1995" doi: "http://www.elsevier.com/gej-ng/31/29/23/26/23/show/Products/notes/index.htt#029" links: doi: "http://www.elsevier.com/gej-ng/31/29/23/26/23/show/Products/notes/index.htt#029" researchr: "https://researchr.org/publication/PfenningW95" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "1" pages: "515-534" kind: "article" key: "PfenningW95" - title: "Metacircularity in the Polymorphic lambda-Calculus" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Peter Lee" link: "https://researchr.org/alias/peter-lee" year: "1991" researchr: "https://researchr.org/publication/PfenningL91" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "89" number: "1" pages: "137-159" kind: "article" key: "PfenningL91" - title: "Refinement Types as Proof Irrelevance" author: - name: "William Lovas" link: "https://researchr.org/alias/william-lovas" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2009" doi: "http://dx.doi.org/10.1007/978-3-642-02273-9_13" links: doi: "http://dx.doi.org/10.1007/978-3-642-02273-9_13" tags: - "refinement" researchr: "https://researchr.org/publication/LovasP09" cites: 0 citedby: 0 pages: "157-171" booktitle: "Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings" editor: - name: "Pierre-Louis Curien" link: "https://researchr.org/alias/pierre-louis-curien" volume: "5608" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-02272-2" kind: "inproceedings" key: "LovasP09" - title: "Analytic and Non-analytic Proofs" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "1984" researchr: "https://researchr.org/publication/Pfenning84" cites: 0 citedby: 0 pages: "394-413" booktitle: "7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings" editor: - name: "Robert E. Shostak" link: "https://researchr.org/alias/robert-e.-shostak" volume: "170" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-96022-8" kind: "inproceedings" key: "Pfenning84" - title: "Linear Logical Relations for Session-Based Concurrency" author: - name: "Jorge A. Pérez" link: "https://researchr.org/alias/jorge-a.-p%C3%A9rez" - name: "Luís Caires" link: "https://researchr.org/alias/lu%C3%ADs-caires" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Bernardo Toninho" link: "https://researchr.org/alias/bernardo-toninho" year: "2012" doi: "http://dx.doi.org/10.1007/978-3-642-28869-2_27" links: doi: "http://dx.doi.org/10.1007/978-3-642-28869-2_27" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/PerezCPT12" researchr: "https://researchr.org/publication/PerezCPT12" cites: 0 citedby: 0 pages: "539-558" booktitle: "Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings" editor: - name: "Helmut Seidl" link: "https://researchr.org/alias/helmut-seidl" volume: "7211" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-28868-5" kind: "inproceedings" key: "PerezCPT12" - title: "Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems" author: - name: "Uluc Saranli" link: "https://researchr.org/alias/uluc-saranli" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2007" doi: "http://dx.doi.org/10.1109/ROBOT.2007.364046" links: doi: "http://dx.doi.org/10.1109/ROBOT.2007.364046" tags: - "logic" researchr: "https://researchr.org/publication/SaranliP07" cites: 0 citedby: 0 pages: "3705-3710" booktitle: "2007 IEEE International Conference on Robotics and Automation, ICRA 2007, 10-14 April 2007, Roma, Italy" publisher: "IEEE" kind: "inproceedings" key: "SaranliP07" - title: "A monadic analysis of information flow security with mutable state" author: - name: "Karl Crary" link: "https://researchr.org/alias/karl-crary" - name: "Aleksey Kliger" link: "https://researchr.org/alias/aleksey-kliger" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2005" doi: "http://dx.doi.org/10.1017/S0956796804005441" links: doi: "http://dx.doi.org/10.1017/S0956796804005441" tags: - "analysis" - "data-flow" - "security" - "data-flow analysis" researchr: "https://researchr.org/publication/CraryKP05" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "15" number: "2" pages: "249-291" kind: "article" key: "CraryKP05" - title: "Focusing the Inverse Method for Linear Logic" author: - name: "Kaustuv Chaudhuri" link: "https://researchr.org/alias/kaustuv-chaudhuri" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2005" doi: "http://dx.doi.org/10.1007/11538363_15" links: doi: "http://dx.doi.org/10.1007/11538363_15" tags: - "logic" researchr: "https://researchr.org/publication/ChaudhuriP05%3A0" cites: 0 citedby: 0 pages: "200-215" booktitle: "Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings" editor: - name: "C.-H. Luke Ong" link: "https://researchr.org/alias/c.-h.-luke-ong" volume: "3634" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-28231-9" kind: "inproceedings" key: "ChaudhuriP05:0" - title: "Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory" author: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" year: "2001" tags: - "type theory" researchr: "https://researchr.org/publication/Pfenning01%3A0" cites: 0 citedby: 0 pages: "221-230" booktitle: "LICS" kind: "inproceedings" key: "Pfenning01:0" - title: "Logic Programming and Automated Reasoning, 5th International Conference, LPAR 94, Kiev, Ukraine, July 16-22, 1994, Proceedings" year: "1994" tags: - "logic programming" - "programming" - "logic" researchr: "https://researchr.org/publication/lpar%3A1994" cites: 0 citedby: 0 booktitle: "Logic Programming and Automated Reasoning, 5th International Conference, LPAR 94, Kiev, Ukraine, July 16-22, 1994, Proceedings" conference: "lpar" editor: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" volume: "822" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-58216-9" kind: "proceedings" key: "lpar:1994" - title: "Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings" year: "2006" tags: - "term rewriting" - "graph-rewriting" - "rewriting" researchr: "https://researchr.org/publication/rta%3A2006" cites: 0 citedby: 0 booktitle: "Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings" conference: "RTA" editor: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" volume: "4098" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-36834-5" kind: "proceedings" key: "rta:2006" - title: "Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, Montreal, Canada, September 20-23, 2000" year: "2000" doi: "https://doi.org/10.1145/351268" links: doi: "https://doi.org/10.1145/351268" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ppdp/2000" researchr: "https://researchr.org/publication/ppdp-2000" cites: 0 citedby: 0 booktitle: "Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, Montreal, Canada, September 20-23, 2000" conference: "ppdp" editor: - name: "Maurizio Gabbrielli" link: "https://researchr.org/alias/maurizio-gabbrielli" - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" publisher: "ACM" isbn: "1-58113-265-4" kind: "proceedings" key: "ppdp-2000" - title: "Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings" year: "2003" tags: - "generative programming" - "programming" researchr: "https://researchr.org/publication/gpce%3A2003" cites: 0 citedby: 0 booktitle: "Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings" conference: "GPCE" editor: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Yannis Smaragdakis" link: "http://smaragd.org" volume: "2830" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-20102-5" kind: "proceedings" key: "gpce:2003" - title: "Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings" year: "2007" researchr: "https://researchr.org/publication/cade%3A2007" cites: 0 citedby: 0 booktitle: "Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings" conference: "cade" editor: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" volume: "4603" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-73594-6" kind: "proceedings" key: "cade:2007" - title: "Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-642-37075-5" links: doi: "http://dx.doi.org/10.1007/978-3-642-37075-5" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fossacs/2013" researchr: "https://researchr.org/publication/fossacs-2013" cites: 0 citedby: 0 booktitle: "Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings" conference: "fossacs" editor: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" volume: "7794" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-37074-8" kind: "proceedings" key: "fossacs-2013"