|
Frank Pfenning
|
| Contents |
2023 | 2022
| 2021 | 2020 2019 | 2018 | 2017 | 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 2000 1999 | 1998 | 1997 | 1996 | 1995 | 1994 | 1993 | 1992 | 1991 | 1990 1989 | 1988 | 1987 | 1986 | 1985 | 1984 |
|---|---|
| Elsewhere | Recent Drafts | BibTeX Source |
Luiz de Sá, Bernardo Toninho, and Frank Pfenning. Intuitionistic metric temporal logic. In S. Escobar, editor, 25th International Symposium on Principles and Practice of Declarative Programming (PPDP 2023), Cascais, Portugal, October 2023. To appear. [ bib | .pdf ]
Henry DeYoung, Andreia Mordido, Frank Pfenning, and Ankush Das. Parametric subtyping for structural parametric polymorphism. CoRR, abs/2307.13661, July 2023. Submitted. [ bib | http | .pdf ]
Siva Somayyajula and Frank Pfenning. Dependent type refinements for futures. In M. Kerjean and P. Levy, editors, 39th International Conference on Mathematical Foundations of Programming Semantics (MFPS 2023), Bloomington, Indiana, USA, June 2023. Preliminary version. [ bib | .pdf ]
Frank Pfenning and Klaas Pruiksma. Relating message passing and shared memory, proof-theoretically. In S. Jongmans and A. Lopes, editors, 25th International Conference on Coordination Models and Languages (COORDINATION 2023), pages 3–27, Lisbon, Portugal, June 2023. Springer LNCS 13908. Notes to an invited talk. [ bib | .pdf ]
Zhibo Chen and Frank Pfenning. A logical framework with higher-order rational (circular) terms. In O. Kupferman and P. Sobocinski, editors, 26th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2023), pages 68–88, Paris, France, April 2023. Springer LNCS 13992. [ bib | .pdf ]
Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, and Frank Pfenning. Polarized subtyping. In Ilya Sergey, editor, 31st European Symposium on Programming (ESOP 2022), pages 431–461, Munich, Germany, April 2022. Springer LNCS 13240. [ bib | .pdf ]
Klaas Pruiksma and Frank Pfenning. Back to futures. Journal of Functional Programming, 32:e6, 2022. [ bib | .pdf ]
Hannah Gommerstadt, Limin Jia, and Frank Pfenning. Session-typed concurrent contracts. Journal of Logical and Algebraic Methods in Programming, 124(100731), January 2022. Special issue on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES 2020). [ bib | .pdf ]
Farzaneh Derakhshan and Frank Pfenning. Circular proofs as session-typed processes: A local validity condition. Logical Methods in Computer Science, 18(2):8:1–8:51, 2022. [ bib | .pdf ]
Henry DeYoung and Frank Pfenning. Data layout from a type-theoretic perspective. In 38th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2022). Electronic Notes in Theoretical Informatics and Computer Science 1, 2022. Invited paper. Extended version available at https://arxiv.org/abs/2212.06321v3.pdf. [ bib | http | .pdf ]
Ankush Das and Frank Pfenning. Rast: A language for resource-aware session types. Logical Methods in Computer Science, 18(1):9:1–9:36, 2022. [ bib | .pdf ]
Bernardo Toninho, Luís Caires, and Frank Pfenning. A decade of dependent session types. In N. Veltri, N. Benton, and S. Ghilezan, editors, 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021), pages 3:1–3:3, Tallinn, Estonia, September 2021. ACM. [ bib | .pdf ]
Chuta Sano, Stephanie Balzer, and Frank Pfenning. Manifestly phased communication via shared session types. In F. Damiani and O. Dardha, editors, 23rd International Conference on Coordination Models and Languages (COORDINATION 2021), pages 23–40, Valletta, Malta, June 2021. Springer LNCS 12717. [ bib | .pdf ]
Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, and Ishani Santurkar. Resource-aware session types for digital contracts. In R. Küsters and D. Naumann, editors, 34th Computer Security Foundations Symposium (CSF 2021), pages 1–16, Dubrovnik, Croatia, June 2021. IEEE. [ bib | .pdf ]
Ankush Das, Henry DeYoung, Andreia Mordido, and Frank Pfenning. Nested session types. In N. Yoshida, editor, 30th European Symposium on Programming, Luxembourg, Luxembourg, March 2021. Springer LNCS. Extended version available as arXiv:2010.06482. [ bib | .pdf | .pdf ]
Ankush Das, Henry DeYoung, Andreia Mordido, and Frank Pfenning. Subtyping on nested polymorphic session types. CoRR, abs/2103.15193, March 2021. [ bib | http | .pdf ]
Klaas Pruiksma and Frank Pfenning. A message-passing interpretation of adjoint logic. Journal of Logical and Algebraic Methods in Programming, 120(100637), 2021. [ bib | .pdf ]
Ankush Das and Frank Pfenning. Verified linear session-typed concurrent programming. In 22nd International Symposium on Principles and Practice of Declarative Programming (PPDP 2020), pages 7:1–7:15, Bologna, Italy, September 2020. ACM. [ bib | .pdf ]
Ankush Das and Frank Pfenning. Session types with arithmetic refinements. In I. Konnov and L. Kovács, editors, 31st International Conference on Concurrency Theory (CONCUR 2020), pages 13:1–13:18, Vienna, Austria, September 2020. LIPIcs 171. [ bib | .pdf ]
Henry DeYoung, Frank Pfenning, and Klaas Pruiksma. Semi-axiomatic sequent calculus. In Z. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), pages 29:1–29:22, Paris, France, June 2020. LIPIcs 167. [ bib | .pdf ]
Ankush Das and Frank Pfenning. Rast: Resource-aware session types with arithmetic refinements. In Z. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), pages 33:1–33:17. LIPIcs 167, June 2020. System description. [ bib | .pdf ]
Farzaneh Derakhshan and Frank Pfenning. Circular proofs in first-order linear logic with least and greatest fixed points. CoRR, abs/2001.05132, January 2020. [ bib | arXiv | .pdf ]
Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Domain-aware session types. In W. Fokkink andk R. van Glabbeek, editor, 30th International Conference on Concurrency Theory (CONCUR 2019), pages 39:1–39:17, Amsterdam, The Netherlands, August 2019. LIPIcs 140. Extended version at CoRR abs/1907.01318. [ bib | extd | .pdf ]
Klaas Pruiksma and Frank Pfenning. A message-passing interpretation of adjoint logic. In F. Martins and D. Orchard, editors, Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES), pages 60–79, Prague, Czech Republic, April 2019. EPTCS 291. [ bib | .pdf ]
Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest deadlock-freedom for shared session types. In L. Caires, editor, 28th European Symposium on Programming (ESOP 2019), pages 611–639, Prague, Czech Republic, April 2019. Springer LNCS 11423. [ bib | .pdf ]
Iliano Cervesato, Thomas J. Cortina, Frank Pfenning, and Saquib Razak. An approach to teaching to write safe and correct imperative programs –- even in C. Unpublished manuscript, January 2019. [ bib ]
Ankush Das, Jan Hoffmann, and Frank Pfenning. Parallel complexity analysis with temporal session types. In M. Flatt, editor, Proceedings of International Conference on Functional Programming (ICFP'18), pages 91:1–91:30, St. Louis, Missouri, USA, September 2018. ACM. [ bib | .pdf ]
Stephanie Balzer, Frank Pfenning, and Bernardo Toninho. A universal session type for untyped asynchronous communication. In S. Schewe and L. Zhang, editors, 29th International Conference on Concurrency Theory (CONCUR'18), pages 30:1–30:18, Beijing, China, September 2018. LIPIcs 118. [ bib | .pdf ]
Iliano Cervesato, Thomas J. Cortina, Frank Pfenning, and Saquib Razak. An approach to teaching to write safe and correct imperative programs — even in C. Unpublished manuscript, August 2018. [ bib | .pdf ]
Ankush Das, Jan Hoffmann, and Frank Pfenning. Work analysis with resource-aware session types. In Anuj Dawar and Erich Grädel, editors, Proceedings of 33rd Symposium on Logic in Computer Science (LICS'18), pages 305–314, Oxford, UK, July 2018. [ bib | .pdf ]
Klaas Pruiksma, William Chargin, Frank Pfenning, and Jason Reed. Adjoint logic. Unpublished manuscript, April 2018. [ bib | .pdf ]
Hannah Gommerstadt, Limin Jia, and Frank Pfenning. Session-typed concurrent contracts. In A. Ahmed, editor, European Symposium on Programming (ESOP'18), pages 771–798, Thessaloniki, Greece, April 2018. Springer LNCS 10801. [ bib | .pdf ]
Stephanie Balzer and Frank Pfenning. Manifest sharing with session types. In International Conference on Functional Programming (ICFP), pages 37:1–37:29. ACM, September 2017. Extended version available as Technical Report CMU-CS-17-106R, June 2017. [ bib | .pdf ]
Henry DeYoung and Frank Pfenning. Substructural proofs as automata. In A. Igarashi, editor, 14th Asian Symposium on Programming Languages and Systems, pages 3–22, Hanoi, Vietnam, November 2016. Springer LNCS 10017. Invited talk. [ bib | .pdf ]
Max Willsey, Rokhini Prabhu, and Frank Pfenning. Design and implementation of Concurrent C0. In Fourth International Workshop on Linearity, pages 73–82. EPTCS 238, June 2016. [ bib | .pdf ]
Miguel Silva, Mário Florido, and Frank Pfenning. Non-blocking concurrent imperative programming with session types. In Fourth International Workshop on Linearity, pages 64–72. EPTCS 238, June 2016. [ bib | .pdf ]
Limin Jia, Hannah Gommerstadt, and Frank Pfenning. Monitors and blame assignment for higher-order session types. In 43rd Annual Symposium on Principles of Programming Languages, pages 582–594, St. Petersburg, Florida, January 2016. ACM Press. [ bib | .pdf ]
Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367–423, 2016. Special Issue on Behavioural Types. [ bib | .pdf ]
Frank Pfenning and Dennis Griffith. Polarized substructural session types. In A. Pitts, editor, Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015), pages 3–22, London, England, April 2015. Springer LNCS 9034. Invited talk. [ bib | .pdf ]
Stephanie Balzer and Frank Pfenning. Objects as session-typed processes. In Workshop on Programming based on Actors, Agents, and Decentralized Control (AGERE! 2015), pages 13–24. ACM SIGPLAN, 2015. [ bib | .pdf ]
Bernardo Toninho, Luís Caires, and Frank Pfenning. Corecursion and non-divergence in session-typed processes. In M. Maffei and E. Tuosto, editors, Proceedings of the 9th International Symposium on Trustworthy Global Computing (TGC 2014), pages 159–175, Rome, Italy, September 2014. Springer LNCS 8902. [ bib | .pdf ]
Flávio Cruz, Ricardo Rocha, Seth Copen Goldstein, and Frank Pfenning. A linear logic programming language for concurrent programming over graph structures. Theory and Practice of Logic Programming, 14(4–5):493–507, July 2014. Special issue dedicated to the 30th International Conference on Logic Programming (ICLP'14). Best Paper Award. [ bib | .pdf ]
Frank Pfenning. Programming with Higher-Order Logic, by dale miller and gopalan nadathur, cambridge university press, 2012. Theory and Practice of Logic Programming, 14(2):265–267, 2014. Book review. [ bib | .pdf ]
Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254–302, 2014. [ bib | .pdf ]
Bernardo Toninho, Luís Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: A monadic integration. In M.Felleisen and P.Gardner, editors, Proceedings of the European Symposium on Programming (ESOP'13), pages 350–369, Rome, Italy, March 2013. Springer LNCS 7792. [ bib | .pdf ]
Frank Pfenning, editor. Proceedings of the 16th International Conference on Foundations of Software Science and Computation Structures, ETAPS 2013, Rome, Italy, March 2013. Springer LNCS 7794. [ bib ]
Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. In M.Felleisen and P.Gardner, editors, Proceedings of the European Symposium on Programming (ESOP'13), pages 330–349, Rome, Italy, March 2013. Springer LNCS 7792. [ bib | .pdf ]
Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut reduction in linear logic as asynchronous session-typed communication. In P. Cégielski and A. Durand, editors, Proceedings of the 21st Conference on Computer Science Logic, CSL 2012, pages 228–242, Fontainebleau, France, September 2012. Leibniz International Proceedings in Informatics. [ bib | .pdf ]
Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann, and Robert J. Simmons. Trace matching in a concurrent logical framework. In A. Chlipala and C. Schürmann, editors, Proceedings of the 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, Copenhagen, Denmark, September 2012. ACM. [ bib | .pdf ]
Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann, and Robert J. Simmons. On matching concurrent traces. In S. Escobar, K. Korovin, and V. Rybakov, editors, Proceedings of the 26th International Workshop on Unification, July 2012. [ bib | .pdf ]
Bernardo Toninho, Luís Caires, and Frank Pfenning. Functions as session-typed processes. In L. Birkedal, editor, 15th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS'12, pages 346–360, Tallinn, Estonia, March 2012. Springer LNCS. [ bib | .pdf ]
Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Termination in session-based concurrency via linear logical relations. In H. Seidl, editor, 22nd European Symposium on Programming, ESOP'12, pages 539–558, Tallinn, Estonia, March 2012. Springer LNCS 7211. [ bib | .pdf ]
Deepak Garg and Frank Pfenning. Stateful authorization logic–-proof theory and a case study. Journal of Computer Security, 20(4):353–391, 2012. [ bib | .pdf ]
Flávio Cruz, Michael Ashley-Rollman, Seth Copen Goldstein inad Ricardo Rocha, and Frank Pfenning. Bottom-up logic programming for multicores. In Proceedings of the Workshop on Declarative Aspects of Multicore Programming, DAMP'12, Philadelphia, PA, January 2012. ACM Press. Short paper. [ bib | .pdf ]
Luís Caires, Frank Pfenning, and Bernardo Toninho. Towards concurrent type theory. In B. Pierce, editor, Proceedings of the 7th Workshop for Types in Language Design and Implementation, TLDI'12, pages 1–12, Philadelphia, Pennsylvania, January 2012. ACM. Notes for an invited talk. [ bib | .pdf ]
Frank Pfenning, Luís Caires, and Bernardo Toninho. Proof-carrying code in a session-typed process calculus. In 1st International Conference on Certified Programs and Proofs, CPP'11, pages 21–36, Kenting, Taiwan, December 2011. Springer LNCS 7086. [ bib | .pdf ]
Frank Pfenning, Thomas J. Cortina, and William Lovas. Teaching imperative programming with contracts at the freshmen level. Experience report. Unpublished manuscript, September 2011. [ bib | .pdf ]
Bernardo Toninho, Luís Caires, and Frank Pfenning. Dependent session types via intuitionistic linear type theory. In Proceedings of the 13th International Conference on Principles and Practice of Declarative Programming, PPDP'11, pages 161–172, Odense, Denmark, July 2011. ACM. [ bib | .pdf ]
Robert J. Simmons, Bernardo Toninho, and Frank Pfenning. Distributed deductive databases, declaratively. Short paper, ACM SIGPLAN X10 Workshop, June 2011. [ bib | .pdf ]
Jamie Morgenstern, Deepak Garg, and Frank Pfenning. A proof-carrying file system with revocable and use-once certificates. In C.Meadows and C.Fernandez-Gago, editors, Proceedings of the 7th International Workshop on Security and Trust Management (STM 2011), Copenhagen, Denmark, June 2011. Springer LNCS. [ bib | .pdf ]
Robert J. Simmons and Frank Pfenning. Weak focusing for ordered linear logic. Technical Report CMU-CS-10-147, Carnegie Mellon University, 2011. Revision of April 2011. [ bib | .pdf ]
Robert J. Simmons and Frank Pfenning. Logical approximation for program analysis. Higher-Order and Symbolic Computation, 24(1–2):41–80, 2011. [ bib | .pdf ]
William Lovas and Frank Pfenning. Refinement types for logical frameworks and their interpretation as proof irrelevance. Logical Methods in Computer Science, 6(4):1–50, December 2010. [ bib | .pdf ]
Deepak Garg and Frank Pfenning. Stateful authorization logic –- proof theory and a case study. In J.Cuellar and J.Lopez, editors, Proceedings of the 6th International Workshop on Security and Trust Management (STM'10), Athens, Greece, September 2010. Springer LNCS. [ bib | .pdf ]
Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010), pages 222–236, Paris, France, August 2010. Springer LNCS 6269. [ bib | .pdf ]
Frank Pfenning. The practice and promise of substructural frameworks. In K.Crary and M.Miculan, editors, Proceedings of 5th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2010), pages 1–2, Edinburgh, Scotland, July 2010. Abstract of invited talk. [ bib ]
Frank Pfenning. Possession as linear knowledge. In B.Farwer, editor, Proceedings of the 3rd International Workshop on Logics, Agents, and Mobility (LAM 2010), Edinburgh, Scotland, July 2010. Abstract of invited talk. [ bib | .pdf ]
Deepak Garg and Frank Pfenning. A proof-carrying file system. In D.Evans and G.Vigna, editors, Proceedings of the 31st Symposium on Security and Privacy (Oakland 2010), pages 349–364, Berkeley, California, May 2010. IEEE. Extended version available as Technical Report CMU-CS-09-123, June 2009. [ bib | .pdf ]
Jason C. Reed and Frank Pfenning. Focus-preserving embeddings of substructural logics in intuitionistic logic. Unpublished Manuscript, January 2010. [ bib | .pdf ]
Frank Pfenning and Robert J. Simmons. Substructural operational semantics as ordered logic programming. In Proceedings of the 24th Annual Symposium on Logic in Computer Science (LICS 2009), pages 101–110, Los Angeles, California, August 2009. IEEE Computer Society Press. [ bib | .pdf ]
Sean McLaughlin and Frank Pfenning. Efficient intuitionistic theorem proving with the polarized inverse method. In R.A.Schmidt, editor, Proceedings of the 22nd International Conference on Automated Deduction (CADE-22)), pages 230–244, Montreal, Canada, August 2009. Springer LNCS 5663. [ bib | .pdf ]
Henry DeYoung and Frank Pfenning. Reasoning about the consequences of authorization policies in a linear epistemic logic. In Workshop on Foundations of Computer Security (FCS'09), Los Angeles, California, August 2009. [ bib | .pdf ]
William Lovas and Frank Pfenning. Refinement types as proof irrelevance. In P.-L. Curien, editor, Proceedings of the 9th International Conference on Typed Lambda Calculi and Applications (TLCA 2009), pages 157–171, Brasilia, Brazil, July 2009. Springer LNCS 5608. [ bib | .pdf ]
Deepak Garg, Frank Pfenning, Denis Serenyi, and Brian Witten. A logical representation of common rule for controlling access to classified information. Technical Report CMU-CS-09-139, Carnegie Mellon University, June 2009. [ bib | .pdf ]
Robert J. Simmons and Frank Pfenning. Linear logical approximations. In G. Puebla and G. Vidal, editors, Proceedings of the Workshop on Partial Evaluation and Program Manipulation, pages 9–20, Savannah, Georgia, January 2009. ACM SIGPLAN. [ bib | .pdf ]
Sungwoo Park, Frank Pfenning, and Sebastian Thrun. A probabilistic language based upon sampling functions. Transactions on Programming Languages and Systems, 31(1), December 2008. [ bib | .pdf ]
Sean McLaughlin and Frank Pfenning. Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. In I.Cervesato, H.Veith, and A.Voronkov, editors, Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), pages 174–181, Doha, Qatar, November 2008. Springer LNCS 5330. System Description. [ bib | .pdf ]
Robert J. Simmons and Frank Pfenning. Linear logical algorithms. In Proceedings of the 35th International Colloquium on Automata, Languages and Programming (ICALP'08), pages 336–345, Reykjavik, Iceland, July 2008. Springer LNCS 5126. [ bib | .pdf ]
F. Pfenning, editor. Proceedings of the 23rd Annual Symposium on Logic in Computer Science (LICS 2008), Pittsburgh, Pennsylvania, June 2008. IEEE Computer Society Press. [ bib ]
Henry DeYoung, Deepak Garg, and Frank Pfenning. An authorization logic with explicit time. In Proceedings of the 21st Computer Security Foundations Symposium (CSF-21), pages 133–145, Pittsburgh, Pennsylvania, June 2008. IEEE Computer Society Press. Extended version available as Technical Report CMU-CS-07-166, revised February 2008. [ bib | .pdf ]
Frank Pfenning. Church and Curry: Combining intrinsic and extrinsic typing. In C.Benzmüller, C.Brown, J.Siekmann, and R.Statman, editors, Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic 17, pages 303–338. College Publications, 2008. [ bib | .pdf ]
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. Transactions on Computational Logic, 9(3), 2008. [ bib | .pdf ]
Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. Journal of Automated Reasoning, 40(2–3):133–177, 2008. Special issue with selected papers from IJCAR 2006. [ bib | .pdf ]
Henry DeYoung, Deepak Garg, and Frank Pfenning. An authorization logic with explicit time. Technical Report CMU-CS-07-166, Carnegie Mellon University, Department of Computer Science, December 2007. Revised February 2008. [ bib | .pdf ]
Jason Reed and Frank Pfenning. Intuitionistic letcc via labelled deduction. In Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007), pages 91–111, Cachan, France, November 2007. Electronic Notes in Theoretical Computer Science (ENTCS), vol 213, March 2009. [ bib | .pdf ]
Frank Pfenning. Subtyping and intersection types revisited. In R. Hinze and N. Ramsey, editors, Proceedings of the 12th International Symposium on Functional Programming (ICFP 2007), page 219, Freiburg, Germany, October 2007. ACM Press. Abstract of invited talk. [ bib ]
F. Pfenning, editor. Proceedings of the 21st International Conference on Automated Deduction (CADE-21), Bremen, Germany, July 2007. Springer LNCS 4603. [ bib ]
William Lovas and Frank Pfenning. A bidirectional refinement type system for LF. In B. Pientka and C. Schürmann, editors, Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pages 113–128, Bremen, Germany, July 2007. Electronic Notes in Theoretical Computer Science (ENTCS), vol 196. [ bib | .pdf ]
Frank Pfenning. On a logical foundation for explicit substitutions. In S. Ronchi Della Rocca, editor, Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications (TLCA 2007), page 1, Paris, France, June 2007. Springer LNCS 4583. Abstract of TLCA/RTA joint invited talk. [ bib ]
Uluç Saranli and Frank Pfenning. Using constrained intuitionistic linear logic for hybrid robotic planning problems. In Proceedings of the International Conference on Robotics and Automation (ICRA'07), pages 3705–3710, Rome Italy, April 2007. IEEE Computer Society Press. [ bib | .pdf ]
Ruy Ley-Wild and Frank Pfenning. Avoiding causal dependencies via proof irrelevance in a concurrent logical framework. Technical Report CMU-CS-07-107, Carnegie Mellon University, February 2007. [ bib | .pdf ]
Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, and Michael K. Reiter. Consumable credentials in logic-based access-control systems. In Proceedings of the 14th Annual Network and Distributed System Security Symposium (NDSS'07), pages 143–157, San Diego, California, February 2007. Internet Society. Preliminary version available as Technical Report CMU-CYLAB-06-002, Carnegie Mellon University, February 2006. [ bib | .pdf ]
Lujo Bauer, Frank Pfenning, and Michael K. Reiter. Distributed system security via logical frameworks. In Information Security Research: New Methods for Protecting Against Cyber Threats, pages 108–115. Department of Defense, Wiley Publishing, 2007. [ bib ]
Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, and Michael Reiter. A linear logic of affirmation and knowledge. In D. Gollman, J. Meier, and A. Sabelfeld, editors, Proceedings of the 11th European Symposium on Research in Computer Security (ESORICS'06), pages 297–312, Hamburg, Germany, September 2006. Springer LNCS 4189. [ bib | .pdf ]
Frank Pfenning, editor. Proceedings of the 17th International Conference on Rewriting Techniques and Applications, Seattle, Washington, August 2006. Springer Verlag LNCS 4098. [ bib ]
Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), pages 97–111, Seattle, Washington, August 2006. Springer LNCS 4130. [ bib | .pdf ]
Deepak Garg and Frank Pfenning. Non-interference in constructive authorization logic. In J. Guttman, editor, Proceedings of the 19th Computer Security Foundations Workshop (CSFW'06), pages 283–293, Venice, Italy, July 2006. IEEE Computer Society Press. [ bib | .pdf ]
Aleksandar Nanevski and Frank Pfenning. Staged computation with names and necessity. Journal of Functional Programming, 15(6):837–891, November 2005. [ bib | .pdf ]
Frank Pfenning. Towards a type theory of contexts. In Proceedings of the 3rd Workshop on Mechanized Reasoning About Languages with Variable Binding (MERLIN'05), page 1, Tallinn, Estonia, September 2005. ACM Press. Abstract for invited talk. [ bib ]
Deepak Garg and Frank Pfenning. Type-directed concurrency. In M.Abadi and L.de Alfaro, editors, Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), pages 6–20, San Francisco, California, August 2005. Springer Verlag LNCS 3653. [ bib | .pdf ]
Kaustuv Chaudhuri and Frank Pfenning. Focusing the inverse method for linear logic. In L.Ong, editor, Proceedings of the 14th Annual Conference on Computer Science Logic (CSL'05), pages 200–215, Oxford, England, August 2005. Springer Verlag LNCS 3634. [ bib | .pdf ]
Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. Monadic concurrent linear logic programming. In A.Felty, editor, Proceedings of the 7th International Symposium on Principles and Practice of Declarative Programming (PPDP'05), pages 35–46, Lisbon, Portugal, July 2005. ACM Press. [ bib | .pdf ]
Kaustuv Chaudhuri and Frank Pfenning. A focusing inverse method prover for first-order linear logic. In R.Nieuwenhuis, editor, Proceedings of the 20th International Conference on Automated Deduction (CADE-20), pages 69–83, Tallinn, Estonia, July 2005. Springer Verlag LNCS 3632. [ bib | .pdf ]
Karl Crary, Aleksey Kliger, and Frank Pfenning. A monadic analysis of information flow security with mutable state. Journal of Functional Programming, 15(2):249–291, March 2005. Preliminary version available as Technical Report CMU-CS-03-164. [ bib | .pdf ]
Sungwoo Park, Frank Pfenning, and Sebastian Thrun. A probabilistic language based upon sampling functions. In M.Abadi, editor, Conference Record of the 32nd Symposium on Principles of Programming Languages (POPL'05), pages 171–182, Long Beach, California, January 2005. ACM Press. [ bib | .pdf ]
Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. Transactions on Computational Logic, 6:61–101, January 2005. [ bib | .pdf ]
Frank Pfenning. Substructural operational semantics and linear destination-passing style. In W.-N. Chin, editor, Proceedings of the 2nd Asian Symposium on Programming Languages and Systems (APLAS'04), page 196, Taipei, Taiwan, November 2004. Springer-Verlag LNCS 3302. Abstract of invited talk. [ bib | .pdf ]
Penny Anderson and Frank Pfenning. Verifying uniqueness in a logical framework. In K.Slind, A.Bunker, and G.Gopalakrishnan, editors, Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'04), pages 18–33, Park City, Utah, September 2004. Springer LNCS 3223. [ bib | .pdf ]
Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. Specifying properties of concurrent computations in CLF. In C.Schürmann, editor, Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFM'04), Cork, Ireland, July 2004. Electronic Notes in Theoretical Computer Science (ENTCS), vol 199, pp. 133–145, 2008. [ bib | .pdf ]
Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning. A symmetric modal lambda calculus for distributed computing. In H. Ganzinger, editor, Proceedings of the 19th Annual Symposium on Logic in Computer Science (LICS'04), pages 286–295, Turku, Finland, July 2004. IEEE Computer Society Press. Extended version available as Technical Report CMU-CS-04-105. [ bib | .pdf ]
Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework: The propositional fragment. In S. Berardi, M. Coppo, and F. Damiani, editors, Types for Proofs and Programs, pages 355–377. Springer-Verlag LNCS 3085, 2004. Revised selected papers from the Third International Workshop on Types for Proofs and Programs, Torino, Italy, April 2003. [ bib | .pdf ]
Frank Pfenning. Review of “Benjamin C. Pierce: Types and programming languages, The MIT Proess, Cambridge, Massachusetts, 2002”. Bulletin of Symbolic Logic, 10:213–214, 2004. [ bib | .pdf ]
Jana Dunfield and Frank Pfenning. Tridirectional typechecking. In X.Leroy, editor, Conference Record of the 31st Annual Symposium on Principles of Programming Languages (POPL'04), pages 281–292, Venice, Italy, January 2004. ACM Press. Extended version available as Technical Report CMU-CS-04-117, March 2004. [ bib | .pdf ]
Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, and Hongwei Xi. ETPS: A system to help students write formal proofs. Journal of Automated Reasoning, 32(1):75–92, 2004. [ bib ]
Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning. A judgmental analysis of linear logic. Technical Report CMU-CS-03-131R, Carnegie Mellon University, Department of Computer Science, December 2003. [ bib | .pdf ]
Alberto Momigliano and Frank Pfenning. Higher-order pattern complement and the strict lambda-calculus. Transactions on Computational Logic, 4(4), October 2003. [ bib | .pdf ]
Carsten Schürmann and Frank Pfenning. A coverage checking algorithm for LF. In D. Basin and B. Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), pages 120–135, Rome, Italy, September 2003. Springer-Verlag LNCS 2758. [ bib | .pdf ]
Frank Pfenning and Yannis Smaragdakis, editors. Proceedings of the Second International Conference on Generative Programming and Component Engineering. Springer-Verlag LNCS 2830, Erfurt, Germany, September 2003. [ bib ]
Aleksandar Nanevski, Brigitte Pientka, and Frank Pfenning. A modal foundation for meta-variables. In Proceedings of the Second Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN'03), Uppsala, Sweden, August 2003. ACM SIGPLAN. [ bib | .pdf ]
M. Berna, B. Lisien, B. Sellner, G. Gordon, F. Pfenning, , and S. Thrun. A learning algorithm for localizing people based on wireless signal strength that uses labeled and unlabeled data. In Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI'03), Acapulco, Mexico, August 2003. Poster. [ bib | .pdf ]
Brigitte Pientka and Frank Pfenning. Optimizing higher-order pattern unification. In F. Baader, editor, Proceedings of the 19th Conference on Automated Deduction (CADE-19), pages 473–487, Miami Beach, Florida, July 2003. Springer-Verlag LNAI 2741. [ bib | .pdf ]
Jana Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In A.D. Gordon, editor, Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'03), pages 250–266, Warsaw, Poland, April 2003. Springer-Verlag LNCS 2620. [ bib | .pdf ]
Leaf Petersen, Robert Harper, Karl Crary, and Frank Pfenning. A type theory for memory allocation and data layout. In G. Morrisett, editor, Conference Record of the 30th Annual Symposium on Principles of Programming Languages (POPL'03), pages 172–184, New Orleans, Louisiana, January 2003. ACM Press. Extended version available as Technical Report CMU-CS-02-171, December 2002. [ bib | .pdf ]
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Automated techniques for provable safe mobile code. Theoretical Computer Science, 290:1175–1199, 2003. Special issue on Dependable Computing. Preliminary version appeared in the proceedings of the DARPA Information Survivability Conference and Exposition (DISCEX 2000), vol 1, pp. 406–419, Hilton Head Island, South Carolina, January 2000. [ bib | .pdf ]
Kaustuv Chaudhuri and Frank Pfenning. Resource management for the inverse method in linear logic. Draft manuscript, January 2003. [ bib | .pdf ]
Iliano Cervesato and Frank Pfenning. A linear spine calculus. Journal of Logic and Computation, 13(5):639–688, 2003. [ bib | .pdf ]
Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, and Frank Pfenning. Trustless grid computing in ConCert. In M. Parashar, editor, Proceedings of the 3rd International Workshop on Grid Computing (GRID'02), pages 112–125, Baltimore, Maryland, November 2002. Springer-Verlag LNCS 2536. [ bib | .pdf ]
Iliano Cervesato and Frank Pfenning. A linear logical framework. Information & Computation, 179(1):19–75, November 2002. Revised and expanded version of an extended abstract, LICS 1996, pp. 264-275. [ bib | .pdf ]
Frank Pfenning, editor. Proceedings of the 3rd International Workshop on Logical Frameworks and Meta-Languages (LFM'02), volume 70(2) of Electronic Notes in Theoretical Computer Science, Copenhagen, Denmark, July 2002. [ bib ]
Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003. [ bib | .pdf ]
Frank Pfenning. Logical frameworks–-a brief introduction. In H. Schwichtenberg and R. Steinbrüggen, editors, Proof and System-Reliability, volume 62 of NATO Science Series II, pages 137–166. Kluwer Academic Publishers, 2002. Lecture notes from the Marktoberdorf Summer School, July 2001. [ bib | .pdf ]
Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins. A concurrent logical framework II: Examples and applications. Technical Report CMU-CS-02-102, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003. [ bib | .pdf ]
Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Modules matter most. Position paper presented at the NSF Workshop on New Visions for Software Design and Productivity, December 2001. Nashville, Tennessee. [ bib | .pdf ]
Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In J. Halpern, editor, Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS'01), pages 221–230, Boston, Massachusetts, June 2001. IEEE Computer Society Press. [ bib | .pdf ]
Andreas Abel, Bor-Yuh Evan Chang, and Frank Pfenning. Human-readable, machine-verifiable proofs for teaching constructive logic. In Proceedings of the Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs (PTP'01), Siena, Italy, June 2001. [ bib | .pdf ]
Frank Pfenning. Logical frameworks at CMU. ALP Newsletter, 14(2), May 2001. [ bib | .html ]
Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555–604, May 2001. [ bib | .pdf ]
Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning. Primitive recursion for higher-order abstract syntax. Theoretical Computer Science, 266:1–57, 2001. [ bib ]
Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511–540, 2001. Notes to an invited talk at the Workshop on Intuitionistic Modal Logics and Applications (IMLA'99), Trento, Italy, July 1999. [ bib | .pdf ]
Frank Pfenning. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, chapter 17, pages 1063–1147. Elsevier Science and MIT Press, 2001. [ bib | .pdf ]
Frank Pfenning. Reasoning about staged computation. In W. Taha, editor, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation (SAIG 2000), pages 5–6, Montreal, Canada, September 2000. Springer-Verlag LNCS 1924. Abstract of invited talk. [ bib | .pdf ]
Maurizio Gabrielli and Frank Pfenning, editors. Proceedings of the International Conference on Principles and Practice of Declarative Programming (PPDP'00), Ottawa, Canada, September 2000. ACM Press. [ bib ]
Rowan Davies and Frank Pfenning. Intersection types and computational effects. In P. Wadler, editor, Proceedings of the Fifth International Conference on Functional Programming (ICFP'00), pages 198–208, Montreal, Canada, September 2000. ACM Press. [ bib | .pdf ]
Jeff Polakow and Frank Pfenning. Properties of terms in continuation-passing style in an ordered logical framework. In Joëlle Despeyroux, editor, 2nd Workshop on Logical Frameworks and Meta-languages (LFM'00), Santa Barbara, California, June 2000. Proceedings available as INRIA Technical Report. [ bib | .pdf ]
Brigitte Pientka and Frank Pfenning. Termination and reduction checking in the logical framework. In Carsten Schürmann, editor, Workshop on Automation of Proofs by Mathematical Induction, Pittsburgh, Pennsylvania, June 2000. [ bib | .pdf ]
Frank Pfenning. Structural cut elimination I. Intuitionistic and classical logic. Information and Computation, 157(1/2):84–141, March 2000. [ bib | .pdf ]
Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. Theoretical Computer Science, 232(1–2):133–163, February 2000. Special issue on Proof Search in Type-Theoretic Languages, D. Galmiche and D. Pym, editors. [ bib | .pdf ]
Frank Pfenning. On the logical foundations of staged computation. In Julia Lawall, editor, Proceedings of the Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'00), page 33, Boston, Massachusetts, January 2000. ACM Press. Abstract of invited talk. [ bib | .pdf ]
Alberto Momigliano and Frank Pfenning. The relative complement problem for higher-order patterns. In D. De Schreye, editor, Proceedings of the International Conference on Logic Programming (ICLP'99), pages 380–394, Las Cruces, New Mexico, November 1999. MIT Press. [ bib | .pdf ]
Frank Pfenning. Logical and meta-logical frameworks. In G. Nadathur, editor, Proceedings of the International Conference on Principles and Practice of Declarative Programming (PPDP'99), page 206, Paris, France, September 1999. Springer-Verlag LNCS 1702. Abstract of invited talk. [ bib ]
Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of CPS programs. In Andrew Gordon and Andrew Pitts, editors, Proceedings of the Third International Workshop on Higher Order Operational Techniques in Semantics (HOOTS'99), Paris, September 1999. Electronic Notes in Theoretical Computer Science, Volume 26. [ bib | .pdf ]
Mark Plesko and Frank Pfenning. A formalization of the proof-carrying code architecture in a linear logical framework. In A. Pnueli and P. Traverso, editors, Proceedings of the FLoC Workshop on Run-Time Result Verification, Trento, Italy, July 1999. [ bib | .pdf ]
Frank Pfenning and Carsten Schürmann. System description: Twelf –- a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202–206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632. [ bib | .pdf ]
Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), pages 295–309, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581. [ bib | .pdf ]
Jeff Polakow and Frank Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. In Andre Scedrov and Achim Jung, editors, Proceedings of the 15th Conference on Mathematical Foundations of Programming Semantics, pages 449–466, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Science, Volume 20. [ bib | .pdf ]
Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In A. Aiken, editor, Conference Record of the 26th Symposium on Principles of Programming Languages (POPL'99), pages 214–227. ACM Press, January 1999. [ bib | .pdf ]
Jeff Polakow and Frank Pfenning. Ordered linear logic programming. Technical Report CMU-CS-98-183, Department of Computer Science, Carnegie Mellon University, December 1998. [ bib | .pdf ]
Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. Rapport de Recherche 3591, INRIA, December 1998. Preliminary version appeared at JICSLP'96. [ bib | .pdf ]
Philip Wickline, Peter Lee, Frank Pfenning, and Rowan Davies. Modal types as staging specifications for run-time code generation. ACM Computing Surveys, 30(3es), September 1998. [ bib | .pdf ]
Frank Pfenning and Carsten Schürmann. Twelf User's Guide, 1.2 edition, September 1998. Available as Technical Report CMU-CS-98-173, Carnegie Mellon University. [ bib ]
Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286–300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. [ bib | .pdf ]
Frank Pfenning. Reasoning about deductions in linear logic. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 1–2, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. Abstract for invited talk. [ bib | .pdf ]
Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Keith D. Cooper, editor, Proceedings of the Conference on Programming Language Design and Implementation (PLDI'98), pages 249–257, Montreal, Canada, June 1998. ACM Press. [ bib | .pdf ]
Philip Wickline, Peter Lee, and Frank Pfenning. Run-time code generation and modal-ML. In Keith D. Cooper, editor, Proceedings of the Conference on Programming Language Design and Implementation (PLDI'98), pages 224–235, Montreal, Canada, June 1998. ACM Press. [ bib | .pdf ]
Frank Pfenning and Carsten Schürmann. Algorithms for equality and unification in the presence of notational definitions. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types for Proofs and Programs, pages 179–193, Kloster Irsee, Germany, March 1998. Springer-Verlag LNCS 1657. [ bib | .pdf ]
Robert Harper, Peter Lee, and Frank Pfenning. The Fox project: Advanced language technology for extensible systems. Technical Report CMU-CS-98-107, Department of Computer Science, Carnegie Mellon University, January 1998. [ bib | .pdf ]
Robert Harper and Frank Pfenning. A module system for a programming language based on the LF logical framework. Journal of Logic and Computation, 8(1):5–31, 1998. [ bib ]
Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. In Glynn Winskel, editor, Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS'97), pages 422–433, Warsaw, Poland, June 1997. IEEE Computer Society Press. [ bib | .pdf ]
Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In R. Hindley, editor, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97), pages 147–163, Nancy, France, April 1997. Springer-Verlag LNCS 1210. An extended version is available as Technical Report CMU-CS-96-172, Carnegie Mellon University. [ bib | .pdf ]
Iliano Cervesato and Frank Pfenning. A linear spine calculus. Technical Report CMU-CS-97-125, Department of Computer Science, Carnegie Mellon University, April 1997. [ bib | .pdf ]
Frank Pfenning. Computation and Deduction. Cambridge University Press, 1997. In preparation. Draft from April 1997 available electronically. [ bib | .ps ]
Paliath Narendran, Frank Pfenning, and Richard Statman. On the unification problem for Cartesian closed categories. Journal of Symbolic Logic, 62(2):636–647, 1997. [ bib ]
Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In M. Maher, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 259–273, Bonn, Germany, September 1996. MIT Press. [ bib | .pdf ]
Iliano Cervesato and Frank Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 264–275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press. [ bib | .pdf ]
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16(3):321–353, June 1996. [ bib ]
Ekkehard Rohwedder and Frank Pfenning. Mode and termination checking for higher-order logic programs. In Hanne Riis Nielson, editor, Proceedings of the European Symposium on Programming, pages 296–310, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1058. [ bib | .pdf ]
Frank Pfenning. The practice of logical frameworks. In Hélène Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, pages 119–134, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1059. Invited talk. [ bib | .pdf ]
Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. In R. Dyckhoff, H. Herre, and P. Schroeder-Heister, editors, Proceedings of the 5th International Workshop on Extensions of Logic Programming, pages 67–81, Leipzig, Germany, March 1996. Springer-Verlag LNAI 1050. [ bib | .pdf ]
Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Guy Steele, Jr., editor, Proceedings of the 23rd Annual Symposium on Principles of Programming Languages, pages 258–270, St. Petersburg Beach, Florida, January 1996. ACM Press. [ bib | .pdf ]
Frank Pfenning. Structural cut elimination. In D. Kozen, editor, Proceedings of the Tenth Annual Symposium on Logic in Computer Science, pages 156–166, San Diego, California, June 1995. IEEE Computer Society Press. [ bib | .pdf ]
Frank Pfenning and Hao-Chi Wong. On a modal λ-calculus for S4. In S. Brookes and M. Main, editors, Proceedings of the Eleventh Conference on Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, March 1995. Electronic Notes in Theoretical Computer Science, Volume 1, Elsevier. [ bib | .pdf ]
Olivier Danvy and Frank Pfenning. The occurrence of continuation parameters in CPS terms. Technical Report CMU-CS-95-121, Department of Computer Science, Carnegie Mellon University, February 1995. [ bib | .pdf ]
Frank Pfenning. Structural cut elimination in linear logic. Technical Report CMU-CS-94-222, Department of Computer Science, Carnegie Mellon University, December 1994. [ bib | .pdf ]
Frank Pfenning. Logical frameworks. Home page and bibliography on the World-Wide Web, October 1994. [ bib ]
Frank Pfenning, editor. Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, Kiev, Ukraine, July 1994. Springer-Verlag LNAI 822. [ bib ]
Frank Pfenning. Elf: A meta-language for deductive systems. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 811–815, Nancy, France, June 1994. Springer-Verlag LNAI 814. System abstract. [ bib | .pdf ]
Robert Harper, Peter Lee, Frank Pfenning, and Eugene Rollins. A compilation manager for Standard ML of New Jersey. In Didier Rémy, editor, Record of the 1994 ACM SIGPLAN Workshop on ML and it Applications, pages 136–147, Orlando, Florida, June 1994. INRIA Technical Report 2265. Available as Technical Report CMU-CS-94-116. [ bib ]
Michael Kohlhase and Frank Pfenning. Unification in a λ-calculus with intersection types. In Dale Miller, editor, Proceedings of the International Logic Programming Symposium, pages 488–505, Vancouver, Canada, October 1993. MIT Press. [ bib | .pdf ]
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: An interactive and automatic tool for proving theorems of type theory. In Jeffrey J. Joyce and Carl-Johan H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, pages 366–370, Vancouver, B.C., Canada, August 1993. Springer-Verlag LNCS 780. [ bib ]
Paliath Narendran, Frank Pfenning, and Richard Statman. On the unification problem for Cartesian closed categories. In Moshe Vardi, editor, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 57–63, Montreal, Canada, June 1993. [ bib | .pdf ]
Frank Pfenning. Refinement types for logical frameworks. In Herman Geuvers, editor, Informal Proceedings of the Workshop on Types for Proofs and Programs, pages 285–299, Nijmegen, The Netherlands, May 1993. [ bib | .pdf ]
Spiro Michaylov and Frank Pfenning. Higher-order logic programming as constraint logic programming. In Position Papers for the First Workshop on Principles and Practice of Constraint Programming, pages 221–229, Newport, Rhode Island, April 1993. Brown University. [ bib | .pdf ]
Frank Pfenning. On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae, 19(1,2):185–199, 1993. Preliminary version available as Technical Report CMU-CS-92-105, School of Computer Science, Carnegie Mellon University, January 1992. [ bib | .pdf ]
Spiro Michaylov and Frank Pfenning. An empirical study of the runtime behavior of higher-order logic programs. In D. Miller, editor, Proceedings of the Workshop on the λProlog Programming Language, pages 257–271, Philadelphia, Pennsylvania, July 1992. University of Pennsylvania. Available as Technical Report MS-CIS-92-86. [ bib | .pdf ]
Frank Pfenning and Ekkehard Rohwedder. Implementing the meta-theory of deductive systems. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, pages 537–551, Saratoga Springs, New York, June 1992. Springer-Verlag LNAI 607. [ bib | .pdf ]
John Hannan and Frank Pfenning. Compiler verification in LF. In Andre Scedrov, editor, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 407–418, Santa Cruz, California, June 1992. [ bib | .pdf ]
Frank Pfenning. Dependent types in logic programming. In Frank Pfenning, editor, Types in Logic Programming, chapter 10, pages 285–311. MIT Press, Cambridge, Massachusetts, 1992. [ bib ]
Frank Pfenning, editor. Types in Logic Programming. MIT Press, Cambridge, Massachusetts, 1992. [ bib ]
Gopalan Nadathur and Frank Pfenning. The type system of a higher-order logic programming language. In Frank Pfenning, editor, Types in Logic Programming, pages 245–283. MIT Press, 1992. [ bib ]
Scott Dietzen and Frank Pfenning. Higher-order and modal logic as a framework for explanation-based generalization. Machine Learning, 9:23–55, 1992. [ bib ]
Scott Dietzen and Frank Pfenning. A declarative alternative to assert in logic programming. In Vijay Saraswat and Kazunori Ueda, editors, International Logic Programming Symposium, pages 372–386. MIT Press, October 1991. [ bib | .pdf ]
Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74–85, Amsterdam, The Netherlands, July 1991. [ bib | .pdf ]
Spiro Michaylov and Frank Pfenning. Compiling the polymorphic λ-calculus. In Paul Hudak and Neil Jones, editors, Proceedings of the Symposium on Partial Evaluation and Semantics Based Program Manipulation, pages 285–296, New Haven, Connecticut, June 1991. ACM Press. Published in SIGPLAN Notices 26(9), September 1991. [ bib ]
Tim Freeman and Frank Pfenning. Refinement types for ML. In Proceedings of the SIGPLAN '91 Symposium on Language Design and Implementation, pages 268–277, Toronto, Ontario, June 1991. ACM Press. [ bib | .pdf ]
Frank Pfenning and Peter Lee. Metacircularity in the polymorphic λ-calculus. Theoretical Computer Science, 89:137–159, 1991. [ bib ]
Frank Pfenning. Logic programming in the LF logical framework. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149–181. Cambridge University Press, 1991. [ bib | .pdf ]
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991. [ bib ]
Spiro Michaylov and Frank Pfenning. Natural semantics and some of its meta-theory in Elf. In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, pages 299–344, Stockholm, Sweden, January 1991. Springer-Verlag LNAI 596. [ bib | .pdf ]
Conal Elliott and Frank Pfenning. A semi-functional implementation of a higher-order logic programming language. In Peter Lee, editor, Topics in Advanced Language Implementation, pages 289–325. MIT Press, 1991. [ bib | http ]
Frank Pfenning and Daniel Nesmith. Presenting intuitive deductions via symmetric simplification. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 336–350, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449. [ bib | .pdf ]
Amy Felty, Elsa Gunter, Dale Miller, and Frank Pfenning. Tutorial on λProlog. In M.E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, page 682, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449. Abstract. [ bib | .pdf ]
Peter B. Andrews, Sunil Issar, Dan Nesmith, and Frank Pfenning. The TPS theorem proving system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 641–642, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449. System abstract. [ bib | .pdf ]
Frank Pfenning. Types in logic programming. In David H.D. Warren and Peter Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming. MIT Press, June 1990. Abstract of advanced tutorial. [ bib | .pdf ]
Frank Pfenning. Program development through proof transformation. Contemporary Mathematics, 106:251–262, 1990. [ bib | .pdf ]
Robert Harper, Peter Lee, and Frank Pfenning. Foundations of programming: Aspects of research in Ergo. In Computer Science Research Review 1988/1989, pages 29–37. School of Computer Science, Carnegie Mellon University, 1990. [ bib | .pdf ]
Peter Lee, Mark Leone, Spiro Michaylov, and Frank Pfenning. Towards a practical programming language based on the polymorphic lambda calculus. Ergo Report 89–085, School of Computer Science, Carnegie Mellon University, November 1989. [ bib | .pdf ]
Scott Dietzen and Frank Pfenning. Explanation-based learning in logic programming. Ergo Report 89–086, Carnegie Mellon University, November 1989. [ bib ]
Frank Pfenning. Elf: A language for logic definition and verified meta-programming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–322, Pacific Grove, California, June 1989. IEEE Computer Society Press. [ bib | .pdf ]
Scott Dietzen and Frank Pfenning. Higher-order and modal logic as a framework for explanation-based generalization. In Alberto Maria Segre, editor, Sixth International Workshop on Machine Learning, pages 447–449, San Mateo, California, June 1989. Morgan Kaufmann Publishers. Expanded version available as Technical Report CMU-CS-89-160, Carnegie Mellon University. [ bib | .pdf ]
Frank Pfenning and Peter Lee. LEAP: A language with eval and polymorphism. In Proceedings of the International Joint Conference on Theory and Practice in Software Development, pages 345–359, Barcelona, Spain, March 1989. Springer-Verlag LNCS 352. [ bib | .pdf ]
Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proceedings of the Fifth Conference on the Mathematical Foundations of Programming Semantics, Tulane University, New Orleans, Louisiana, pages 209–228. Springer-Verlag LNCS 442, March 1989. [ bib | .pdf ]
Frank Pfenning. Review of “Jean H. Gallier: Logic for Computer Science, Harper & Row, New York 1986”. Journal of Symbolic Logic, 54(1):288–289, March 1989. [ bib ]
Robert L. Nord and Frank Pfenning. The Ergo attribute system. In Peter Henderson, editor, Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pages 110–120. ACM Press, November 1988. [ bib | .pdf ]
Peter Lee, Frank Pfenning, Gene Rollins, and William Scherlis. The Ergo Support System: An integrated set of tools for prototyping integrated environments. In Peter Henderson, editor, Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pages 25–34. ACM Press, November 1988. [ bib | .pdf ]
Frank Pfenning. Partial polymorphic type inference and higher-order unification. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pages 153–163, Snowbird, Utah, July 1988. ACM Press. [ bib | .pdf ]
Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN '88 Symposium on Language Design and Implementation, pages 199–208, Atlanta, Georgia, June 1988. [ bib | .pdf ]
Frank Pfenning. Single axioms in the implicational propositional calculus. In Ewing Lusk and Ross Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction, pages 710–713, Argonne, Illinois, May 1988. Springer-Verlag LNCS 310. Problem set. [ bib | .pdf ]
Peter Lee, Frank Pfenning, John Reynolds, Gene Rollins, and Dana Scott. Research on semantically based program-design environments: The Ergo Project in 1988. Technical Report CMU-CS-88-118, Carnegie Mellon University, March 1988. [ bib | .pdf ]
Conal Elliott and Frank Pfenning. A family of program derivations for higher-order unification. Ergo Report 87–045, Carnegie Mellon University, November 1987. [ bib | .pdf ]
Frank Pfenning. Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University, January 1987. [ bib | .pdf ]
Peter B. Andrews, Dale Miller, Eve Cohen, and Frank Pfenning. Automating higher-order logic. Contemporary Mathematics, 29:169–192, August 1984. [ bib | .pdf ]
Frank Pfenning. Analytic and non-analytic proofs. In R.E. Shostak, editor, Proceedings of the 7th Conference on Automated Deduction, pages 394–413, Napa, California, May 1984. Springer-Verlag LNCS 170. [ bib | .pdf ]
[ Home
| Contact
| Research
| Publications
| CV
| Students
]
[ Projects
| Courses
| Conferences
| Organizations
| Journals
]