Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Frank Pfenning
@article{DBLP:journals/pacmpl/DeYoungMPD24,
author = {Henry DeYoung and
Andreia Mordido and
Frank Pfenning and
Ankush Das},
title = {Parametric Subtyping for Structural Parametric Polymorphism},
journal = {Proc. {ACM} Program. Lang.},
volume = {8},
number = {{POPL}},
pages = {2700--2730},
year = {2024}
}
@article{DBLP:journals/corr/abs-2402-01428,
author = {Junyoung Jang and
Sophia Roshal and
Frank Pfenning and
Brigitte Pientka},
title = {Adjoint Natural Deduction (Extended Version)},
journal = {CoRR},
volume = {abs/2402.01428},
year = {2024}
}
@inproceedings{DBLP:conf/coordination/PfenningP23,
author = {Frank Pfenning and
Klaas Pruiksma},
title = {Relating Message Passing and Shared Memory, Proof-Theoretically},
booktitle = {{COORDINATION}},
series = {Lecture Notes in Computer Science},
volume = {13908},
pages = {3--27},
publisher = {Springer},
year = {2023}
}
@inproceedings{DBLP:conf/fossacs/ChenP23,
author = {Zhibo Chen and
Frank Pfenning},
title = {A Logical Framework with Higher-Order Rational (Circular) Terms},
booktitle = {FoSSaCS},
series = {Lecture Notes in Computer Science},
volume = {13992},
pages = {68--88},
publisher = {Springer},
year = {2023}
}
@inproceedings{DBLP:conf/ppdp/SaTP23,
author = {Luiz De S{\'{a}} and
Bernardo Toninho and
Frank Pfenning},
title = {Intuitionistic Metric Temporal Logic},
booktitle = {{PPDP}},
pages = {9:1--9:13},
publisher = {{ACM}},
year = {2023}
}
@inproceedings{DBLP:journals/corr/abs-2309-08581,
author = {Siva Somayyajula and
Frank Pfenning},
title = {Dependent Type Refinements for Futures},
booktitle = {{MFPS}},
series = {{EPTICS}},
volume = {3},
publisher = {EpiSciences},
year = {2023}
}
@article{DBLP:journals/corr/abs-2307-13661,
author = {Henry DeYoung and
Andreia Mordido and
Frank Pfenning and
Ankush Das},
title = {Parametric Subtyping for Structural Parametric Polymorphism},
journal = {CoRR},
volume = {abs/2307.13661},
year = {2023}
}
@article{DBLP:journals/corr/abs-2312-07263,
author = {Zhibo Chen and
Frank Pfenning},
title = {A Saturation-Based Unification Algorithm for Higher-Order Rational
Patterns},
journal = {CoRR},
volume = {abs/2312.07263},
year = {2023}
}
@article{DBLP:journals/jfp/PruiksmaP22,
author = {Klaas Pruiksma and
Frank Pfenning},
title = {Back to futures},
journal = {J. Funct. Program.},
volume = {32},
pages = {e6},
year = {2022}
}
@article{DBLP:journals/jlap/GommerstadtJP22,
author = {Hannah Gommerstadt and
Limin Jia and
Frank Pfenning},
title = {Session-typed concurrent contracts},
journal = {J. Log. Algebraic Methods Program.},
volume = {124},
pages = {100731},
year = {2022}
}
@article{DBLP:journals/lmcs/DasP22,
author = {Ankush Das and
Frank Pfenning},
title = {Rast: {A} Language for Resource-Aware Session Types},
journal = {Log. Methods Comput. Sci.},
volume = {18},
number = {1},
year = {2022}
}
@article{DBLP:journals/lmcs/DerakhshanP22,
author = {Farzaneh Derakhshan and
Frank Pfenning},
title = {Circular Proofs as Session-Typed Processes: {A} Local Validity Condition},
journal = {Log. Methods Comput. Sci.},
volume = {18},
number = {2},
year = {2022}
}
@article{DBLP:journals/toplas/DasDMP22,
author = {Ankush Das and
Henry DeYoung and
Andreia Mordido and
Frank Pfenning},
title = {Nested Session Types},
journal = {{ACM} Trans. Program. Lang. Syst.},
volume = {44},
number = {3},
pages = {19:1--19:45},
year = {2022}
}
@inproceedings{DBLP:conf/esop/LakhaniDDMP22,
author = {Zeeshan Lakhani and
Ankush Das and
Henry DeYoung and
Andreia Mordido and
Frank Pfenning},
title = {Polarized Subtyping},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {13240},
pages = {431--461},
publisher = {Springer},
year = {2022}
}
@inproceedings{DBLP:conf/fscd/SomayyajulaP22,
author = {Siva Somayyajula and
Frank Pfenning},
title = {Type-Based Termination for Futures},
booktitle = {{FSCD}},
series = {LIPIcs},
volume = {228},
pages = {12:1--12:21},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022}
}
@inproceedings{DBLP:journals/corr/abs-2212-06321,
author = {Henry DeYoung and
Frank Pfenning},
title = {Data Layout from a Type-Theoretic Perspective (extended version)},
booktitle = {{MFPS}},
series = {{EPTICS}},
volume = {1},
publisher = {EpiSciences},
year = {2022}
}
@article{DBLP:journals/corr/abs-2201-10998,
author = {Zeeshan Lakhani and
Ankush Das and
Henry DeYoung and
Andreia Mordido and
Frank Pfenning},
title = {Polarized Subtyping},
journal = {CoRR},
volume = {abs/2201.10998},
year = {2022}
}
@article{DBLP:journals/corr/abs-2210-06663,
author = {Zhibo Chen and
Frank Pfenning},
title = {A Logical Framework with Higher-Order Rational (Circular) Terms},
journal = {CoRR},
volume = {abs/2210.06663},
year = {2022}
}
@article{DBLP:journals/jlap/PruiksmaP21,
author = {Klaas Pruiksma and
Frank Pfenning},
title = {A message-passing interpretation of adjoint logic},
journal = {J. Log. Algebraic Methods Program.},
volume = {120},
pages = {100637},
year = {2021}
}
@inproceedings{DBLP:conf/coordination/SanoBP21,
author = {Chuta Sano and
Stephanie Balzer and
Frank Pfenning},
title = {Manifestly Phased Communication via Shared Session Types},
booktitle = {{COORDINATION}},
series = {Lecture Notes in Computer Science},
volume = {12717},
pages = {23--40},
publisher = {Springer},
year = {2021}
}
@inproceedings{DBLP:conf/csfw/DasB0PS21,
author = {Ankush Das and
Stephanie Balzer and
Jan Hoffmann and
Frank Pfenning and
Ishani Santurkar},
title = {Resource-Aware Session Types for Digital Contracts},
booktitle = {{CSF}},
pages = {1--16},
publisher = {{IEEE}},
year = {2021}
}
@inproceedings{DBLP:conf/esop/DasDMP21,
author = {Ankush Das and
Henry DeYoung and
Andreia Mordido and
Frank Pfenning},
title = {Nested Session Types},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {12648},
pages = {178--206},
publisher = {Springer},
year = {2021}
}
@inproceedings{DBLP:conf/ppdp/ToninhoCP21,
author = {Bernardo Toninho and
Lu{\'{\i}}s Caires and
Frank Pfenning},
title = {A Decade of Dependent Session Types},
booktitle = {{PPDP}},
pages = {3:1--3:3},
publisher = {{ACM}},
year = {2021}
}
@article{DBLP:journals/corr/abs-2101-06249,
author = {Chuta Sano and
Stephanie Balzer and
Frank Pfenning},
title = {Manifestly Phased Communication via Shared Session Types},
journal = {CoRR},
volume = {abs/2101.06249},
year = {2021}
}
@article{DBLP:journals/corr/abs-2103-15193,
author = {Ankush Das and
Henry DeYoung and
Andreia Mordido and
Frank Pfenning},
title = {Subtyping on Nested Polymorphic Session Types},
journal = {CoRR},
volume = {abs/2103.15193},
year = {2021}
}
@article{DBLP:journals/corr/abs-2105-06024,
author = {Siva Somayyajula and
Frank Pfenning},
title = {Circular Proofs as Processes: Type-Based Termination via Arithmetic
Refinements},
journal = {CoRR},
volume = {abs/2105.06024},
year = {2021}
}
@inproceedings{DBLP:conf/concur/DasP20,
author = {Ankush Das and
Frank Pfenning},
title = {Session Types with Arithmetic Refinements},
booktitle = {{CONCUR}},
series = {LIPIcs},
volume = {171},
pages = {13:1--13:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2020}
}
@inproceedings{DBLP:conf/fscd/DeYoungPP20,
author = {Henry DeYoung and
Frank Pfenning and
Klaas Pruiksma},
title = {Semi-Axiomatic Sequent Calculus},
booktitle = {{FSCD}},
series = {LIPIcs},
volume = {167},
pages = {29:1--29:22},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2020}
}
@inproceedings{DBLP:conf/fscd/DasP20,
author = {Ankush Das and
Frank Pfenning},
title = {Rast: Resource-Aware Session Types with Arithmetic Refinements (System
Description)},
booktitle = {{FSCD}},
series = {LIPIcs},
volume = {167},
pages = {33:1--33:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2020}
}
@inproceedings{DBLP:conf/ppdp/DasP20,
author = {Ankush Das and
Frank Pfenning},
title = {Verified Linear Session-Typed Concurrent Programming},
booktitle = {{PPDP}},
pages = {7:1--7:15},
publisher = {{ACM}},
year = {2020}
}
@article{DBLP:journals/corr/abs-2001-04439,
author = {Ankush Das and
Frank Pfenning},
title = {Session Types with Arithmetic Refinements and Their Application to
Work Analysis},
journal = {CoRR},
volume = {abs/2001.04439},
year = {2020}
}
@article{DBLP:journals/corr/abs-2001-05132,
author = {Farzaneh Derakhshan and
Frank Pfenning},
title = {Circular Proofs in First-Order Linear Logic with Least and Greatest
Fixed Points},
journal = {CoRR},
volume = {abs/2001.05132},
year = {2020}
}
@article{DBLP:journals/corr/abs-2002-04607,
author = {Klaas Pruiksma and
Frank Pfenning},
title = {Back to Futures},
journal = {CoRR},
volume = {abs/2002.04607},
year = {2020}
}
@article{DBLP:journals/corr/abs-2005-05970,
author = {Ankush Das and
Frank Pfenning},
title = {Session Types with Arithmetic Refinements},
journal = {CoRR},
volume = {abs/2005.05970},
year = {2020}
}
@article{DBLP:journals/corr/abs-2010-06482,
author = {Ankush Das and
Henry DeYoung and
Andreia Mordido and
Frank Pfenning},
title = {Nested Session Types},
journal = {CoRR},
volume = {abs/2010.06482},
year = {2020}
}
@article{DBLP:journals/corr/abs-2012-13129,
author = {Ankush Das and
Frank Pfenning},
title = {Rast: {A} Language for Resource-Aware Session Types},
journal = {CoRR},
volume = {abs/2012.13129},
year = {2020}
}
@inproceedings{DBLP:conf/concur/CairesPPT19,
author = {Lu{\'{\i}}s Caires and
Jorge A. P{\'{e}}rez and
Frank Pfenning and
Bernardo Toninho},
title = {Domain-Aware Session Types},
booktitle = {{CONCUR}},
series = {LIPIcs},
volume = {140},
pages = {39:1--39:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2019}
}
@inproceedings{DBLP:conf/esop/BalzerTP19,
author = {Stephanie Balzer and
Bernardo Toninho and
Frank Pfenning},
title = {Manifest Deadlock-Freedom for Shared Session Types},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {11423},
pages = {611--639},
publisher = {Springer},
year = {2019}
}
@inproceedings{DBLP:journals/corr/abs-1904-01290,
author = {Klaas Pruiksma and
Frank Pfenning},
title = {A Message-Passing Interpretation of Adjoint Logic},
booktitle = {PLACES@ETAPS},
series = {{EPTCS}},
volume = {291},
pages = {60--79},
year = {2019}
}
@article{DBLP:journals/corr/abs-1902-06056,
author = {Ankush Das and
Stephanie Balzer and
Jan Hoffmann and
Frank Pfenning},
title = {Resource-Aware Session Types for Digital Contracts},
journal = {CoRR},
volume = {abs/1902.06056},
year = {2019}
}
@article{DBLP:journals/corr/abs-1907-01318,
author = {Lu{\'{\i}}s Caires and
Jorge A. P{\'{e}}rez and
Frank Pfenning and
Bernardo Toninho},
title = {Domain-Aware Session Types (Extended Version)},
journal = {CoRR},
volume = {abs/1907.01318},
year = {2019}
}
@article{DBLP:journals/corr/abs-1908-01909,
author = {Farzaneh Derakhshan and
Frank Pfenning},
title = {Circular Proofs as Session-Typed Processes: {A} Local Validity Condition},
journal = {CoRR},
volume = {abs/1908.01909},
year = {2019}
}
@article{DBLP:journals/pacmpl/Das0P18,
author = {Ankush Das and
Jan Hoffmann and
Frank Pfenning},
title = {Parallel complexity analysis with temporal session types},
journal = {Proc. {ACM} Program. Lang.},
volume = {2},
number = {{ICFP}},
pages = {91:1--91:30},
year = {2018}
}
@inproceedings{DBLP:conf/concur/BalzerPT18,
author = {Stephanie Balzer and
Frank Pfenning and
Bernardo Toninho},
title = {A Universal Session Type for Untyped Asynchronous Communication},
booktitle = {{CONCUR}},
series = {LIPIcs},
volume = {118},
pages = {30:1--30:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2018}
}
@inproceedings{DBLP:conf/esop/GommerstadtJP18,
author = {Hannah Gommerstadt and
Limin Jia and
Frank Pfenning},
title = {Session-Typed Concurrent Contracts},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {10801},
pages = {771--798},
publisher = {Springer},
year = {2018}
}
@inproceedings{DBLP:conf/lics/Das0P18,
author = {Ankush Das and
Jan Hoffmann and
Frank Pfenning},
title = {Work Analysis with Resource-Aware Session Types},
booktitle = {{LICS}},
pages = {305--314},
publisher = {{ACM}},
year = {2018}
}
@article{DBLP:journals/corr/abs-1804-06013,
author = {Ankush Das and
Jan Hoffmann and
Frank Pfenning},
title = {Parallel Complexity Analysis with Temporal Session Types},
journal = {CoRR},
volume = {abs/1804.06013},
year = {2018}
}
@article{DBLP:journals/pacmpl/BalzerP17,
author = {Stephanie Balzer and
Frank Pfenning},
title = {Manifest sharing with session types},
journal = {Proc. {ACM} Program. Lang.},
volume = {1},
number = {{ICFP}},
pages = {37:1--37:29},
year = {2017}
}
@article{DBLP:journals/corr/abs-1712-08310,
author = {Ankush Das and
Jan Hoffmann and
Frank Pfenning},
title = {Work Analysis with Resource-Aware Session Types},
journal = {CoRR},
volume = {abs/1712.08310},
year = {2017}
}
@article{DBLP:journals/mscs/CairesPT16,
author = {Lu{\'{\i}}s Caires and
Frank Pfenning and
Bernardo Toninho},
title = {Linear logic propositions as session types},
journal = {Math. Struct. Comput. Sci.},
volume = {26},
number = {3},
pages = {367--423},
year = {2016}
}
@inproceedings{DBLP:conf/aplas/DeYoungP16,
author = {Henry DeYoung and
Frank Pfenning},
title = {Substructural Proofs as Automata},
booktitle = {{APLAS}},
series = {Lecture Notes in Computer Science},
volume = {10017},
pages = {3--22},
year = {2016}
}
@inproceedings{DBLP:conf/popl/JiaGP16,
author = {Limin Jia and
Hannah Gommerstadt and
Frank Pfenning},
title = {Monitors and blame assignment for higher-order session types},
booktitle = {{POPL}},
pages = {582--594},
publisher = {{ACM}},
year = {2016}
}
@inproceedings{DBLP:journals/corr/AcayP17,
author = {Cosku Acay and
Frank Pfenning},
title = {Intersections and Unions of Session Types},
booktitle = {{ITRS}},
series = {{EPTCS}},
volume = {242},
pages = {4--19},
year = {2016}
}
@inproceedings{DBLP:journals/corr/SilvaFP17,
author = {Miguel E. P. Silva and
M{\'{a}}rio Florido and
Frank Pfenning},
title = {Non-Blocking Concurrent Imperative Programming with Session Types},
booktitle = {{LINEARITY}},
series = {{EPTCS}},
volume = {238},
pages = {64--72},
year = {2016}
}
@inproceedings{DBLP:journals/corr/WillseyPP17,
author = {Max Willsey and
Rokhini Prabhu and
Frank Pfenning},
title = {Design and Implementation of Concurrent {C0}},
booktitle = {{LINEARITY}},
series = {{EPTCS}},
volume = {238},
pages = {73--82},
year = {2016}
}
@inproceedings{DBLP:conf/agere/BalzerP15,
author = {Stephanie Balzer and
Frank Pfenning},
title = {Objects as session-typed processes},
booktitle = {AGERE!@SPLASH},
pages = {13--24},
publisher = {{ACM}},
year = {2015}
}
@inproceedings{DBLP:conf/fossacs/PfenningG15,
author = {Frank Pfenning and
Dennis Griffith},
title = {Polarized Substructural Session Types},
booktitle = {FoSSaCS},
series = {Lecture Notes in Computer Science},
volume = {9034},
pages = {3--22},
publisher = {Springer},
year = {2015}
}
@inproceedings{DBLP:conf/popl/Pfenning15,
author = {Frank Pfenning},
title = {Proof theory and its role in programming language research},
booktitle = {PLMW@POPL},
pages = {4:1},
publisher = {{ACM}},
year = {2015}
}
@article{DBLP:journals/iandc/PerezCPT14,
author = {Jorge A. P{\'{e}}rez and
Lu{\'{\i}}s Caires and
Frank Pfenning and
Bernardo Toninho},
title = {Linear logical relations and observational equivalences for session-based
concurrency},
journal = {Inf. Comput.},
volume = {239},
pages = {254--302},
year = {2014}
}
@article{DBLP:journals/tplp/Pfenning14,
author = {Frank Pfenning},
title = {\emph{Programming with Higher-Order Logic}, by Dale Miller and Gopalan
Nadathur, Cambridge University Press, 2012, Hardcover, {ISBN-10:}
052187940X, xiv + 306 pp},
journal = {Theory Pract. Log. Program.},
volume = {14},
number = {2},
pages = {265--267},
year = {2014}
}
@article{DBLP:journals/tplp/CruzRGP14,
author = {Fl{\'{a}}vio Cruz and
Ricardo Rocha and
Seth Copen Goldstein and
Frank Pfenning},
title = {A Linear Logic Programming Language for Concurrent Programming over
Graph Structures},
journal = {Theory Pract. Log. Program.},
volume = {14},
number = {4-5},
pages = {493--507},
year = {2014}
}
@inproceedings{DBLP:conf/tgc/ToninhoCP14,
author = {Bernardo Toninho and
Lu{\'{\i}}s Caires and
Frank Pfenning},
title = {Corecursion and Non-divergence in Session-Typed Processes},
booktitle = {{TGC}},
series = {Lecture Notes in Computer Science},
volume = {8902},
pages = {159--175},
publisher = {Springer},
year = {2014}
}
@article{DBLP:journals/corr/CruzRGP14,
author = {Fl{\'{a}}vio Cruz and
Ricardo Rocha and
Seth Copen Goldstein and
Frank Pfenning},
title = {A Linear Logic Programming Language for Concurrent Programming over
Graph Structures},
journal = {CoRR},
volume = {abs/1405.3556},
year = {2014}
}
@inproceedings{DBLP:conf/esop/CairesPPT13,
author = {Lu{\'{\i}}s Caires and
Jorge A. P{\'{e}}rez and
Frank Pfenning and
Bernardo Toninho},
title = {Behavioral Polymorphism and Parametricity in Session-Based Communication},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {7792},
pages = {330--349},
publisher = {Springer},
year = {2013}
}
@inproceedings{DBLP:conf/esop/ToninhoCP13,
author = {Bernardo Toninho and
Lu{\'{\i}}s Caires and
Frank Pfenning},
title = {Higher-Order Processes, Functions, and Sessions: {A} Monadic Integration},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {7792},
pages = {350--369},
publisher = {Springer},
year = {2013}
}
@proceedings{DBLP:conf/fossacs/2013,
editor = {Frank Pfenning},
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},
series = {Lecture Notes in Computer Science},
volume = {7794},
publisher = {Springer},
year = {2013}
}
@article{DBLP:journals/jcs/GargP12,
author = {Deepak Garg and
Frank Pfenning},
title = {Stateful authorization logic - Proof theory and a case study},
journal = {J. Comput. Secur.},
volume = {20},
number = {4},
pages = {353--391},
year = {2012}
}
@inproceedings{DBLP:conf/csl/DeYoungCPT12,
author = {Henry DeYoung and
Lu{\'{\i}}s Caires and
Frank Pfenning and
Bernardo Toninho},
title = {Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication},
booktitle = {{CSL}},
series = {LIPIcs},
volume = {16},
pages = {228--242},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2012}
}
@inproceedings{DBLP:conf/esop/PerezCPT12,
author = {Jorge A. P{\'{e}}rez and
Lu{\'{\i}}s Caires and
Frank Pfenning and
Bernardo Toninho},
title = {Linear Logical Relations for Session-Based Concurrency},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {7211},
pages = {539--558},
publisher = {Springer},
year = {2012}
}
@inproceedings{DBLP:conf/fossacs/ToninhoCP12,
author = {Bernardo Toninho and
Lu{\'{\i}}s Caires and
Frank Pfenning},
title = {Functions as Session-Typed Processes},
booktitle = {FoSSaCS},
series = {Lecture Notes in Computer Science},
volume = {7213},
pages = {346--360},
publisher = {Springer},
year = {2012}
}
@inproceedings{DBLP:conf/tldi/CairesPT12,
author = {Lu{\'{\i}}s Caires and
Frank Pfenning and
Bernardo Toninho},
title = {Towards concurrent type theory},
booktitle = {{TLDI}},
pages = {1--12},
publisher = {{ACM}},
year = {2012}
}
@article{DBLP:journals/lisp/SimmonsP11,
author = {Robert J. Simmons and
Frank Pfenning},
title = {Logical approximation for program analysis},
journal = {High. Order Symb. Comput.},
volume = {24},
number = {1-2},
pages = {41--80},
year = {2011}
}
@inproceedings{DBLP:conf/cpp/PfenningCT11,
author = {Frank Pfenning and
Lu{\'{\i}}s Caires and
Bernardo Toninho},
title = {Proof-Carrying Code in a Session-Typed Process Calculus},
booktitle = {{CPP}},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {21--36},
publisher = {Springer},
year = {2011}
}
@inproceedings{DBLP:conf/ppdp/ToninhoCP11,
author = {Bernardo Toninho and
Lu{\'{\i}}s Caires and
Frank Pfenning},
title = {Dependent session types via intuitionistic linear type theory},
booktitle = {{PPDP}},
pages = {161--172},
publisher = {{ACM}},
year = {2011}
}
@inproceedings{DBLP:conf/stm/MorgensternGP11,
author = {Jamie Morgenstern and
Deepak Garg and
Frank Pfenning},
title = {A Proof-Carrying File System with Revocable and Use-Once Certificates},
booktitle = {{STM}},
series = {Lecture Notes in Computer Science},
volume = {7170},
pages = {40--55},
publisher = {Springer},
year = {2011}
}
@article{DBLP:journals/corr/abs-1009-1861,
author = {William Lovas and
Frank Pfenning},
title = {Refinement Types for Logical Frameworks and Their Interpretation as
Proof Irrelevance},
journal = {Log. Methods Comput. Sci.},
volume = {6},
number = {4},
year = {2010}
}
@inproceedings{DBLP:conf/concur/CairesP10,
author = {Lu{\'{\i}}s Caires and
Frank Pfenning},
title = {Session Types as Intuitionistic Linear Propositions},
booktitle = {{CONCUR}},
series = {Lecture Notes in Computer Science},
volume = {6269},
pages = {222--236},
publisher = {Springer},
year = {2010}
}
@inproceedings{DBLP:conf/lics/Pfenning10,
author = {Frank Pfenning},
title = {Possession as Linear Knowledge},
booktitle = {LAM@LICS},
series = {EPiC Series in Computing},
volume = {7},
pages = {1},
publisher = {EasyChair},
year = {2010}
}
@inproceedings{DBLP:conf/sp/GargP10,
author = {Deepak Garg and
Frank Pfenning},
title = {A Proof-Carrying File System},
booktitle = {{IEEE} Symposium on Security and Privacy},
pages = {349--364},
publisher = {{IEEE} Computer Society},
year = {2010}
}
@inproceedings{DBLP:conf/stm/GargP10,
author = {Deepak Garg and
Frank Pfenning},
title = {Stateful Authorization Logic: - Proof Theory and a Case Study},
booktitle = {{STM}},
series = {Lecture Notes in Computer Science},
volume = {6710},
pages = {210--225},
publisher = {Springer},
year = {2010}
}
@inproceedings{DBLP:conf/cade/McLaughlinP09,
author = {Sean McLaughlin and
Frank Pfenning},
title = {Efficient Intuitionistic Theorem Proving with the Polarized Inverse
Method},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {5663},
pages = {230--244},
publisher = {Springer},
year = {2009}
}
@inproceedings{DBLP:conf/lics/PfenningS09,
author = {Frank Pfenning and
Robert J. Simmons},
title = {Substructural Operational Semantics as Ordered Logic Programming},
booktitle = {{LICS}},
pages = {101--110},
publisher = {{IEEE} Computer Society},
year = {2009}
}
@inproceedings{DBLP:conf/pepm/SimmonsP09,
author = {Robert J. Simmons and
Frank Pfenning},
title = {Linear logical approximations},
booktitle = {{PEPM}},
pages = {9--20},
publisher = {{ACM}},
year = {2009}
}
@inproceedings{DBLP:conf/tlca/LovasP09,
author = {William Lovas and
Frank Pfenning},
title = {Refinement Types as Proof Irrelevance},
booktitle = {{TLCA}},
series = {Lecture Notes in Computer Science},
volume = {5608},
pages = {157--171},
publisher = {Springer},
year = {2009}
}
@article{DBLP:journals/jar/ChaudhuriPP08,
author = {Kaustuv Chaudhuri and
Frank Pfenning and
Greg Price},
title = {A Logical Characterization of Forward and Backward Chaining in the
Inverse Method},
journal = {J. Autom. Reason.},
volume = {40},
number = {2-3},
pages = {133--177},
year = {2008}
}
@article{DBLP:journals/tocl/NanevskiPP08,
author = {Aleksandar Nanevski and
Frank Pfenning and
Brigitte Pientka},
title = {Contextual modal type theory},
journal = {{ACM} Trans. Comput. Log.},
volume = {9},
number = {3},
pages = {23:1--23:49},
year = {2008}
}
@article{DBLP:journals/toplas/ParkPT08,
author = {Sungwoo Park and
Frank Pfenning and
Sebastian Thrun},
title = {A probabilistic language based on sampling functions},
journal = {{ACM} Trans. Program. Lang. Syst.},
volume = {31},
number = {1},
pages = {4:1--4:46},
year = {2008}
}
@inproceedings{DBLP:conf/csfw/DeYoungGP08,
author = {Henry DeYoung and
Deepak Garg and
Frank Pfenning},
title = {An Authorization Logic With Explicit Time},
booktitle = {{CSF}},
pages = {133--145},
publisher = {{IEEE} Computer Society},
year = {2008}
}
@inproceedings{DBLP:conf/icalp/SimmonsP08,
author = {Robert J. Simmons and
Frank Pfenning},
title = {Linear Logical Algorithms},
booktitle = {{ICALP} {(2)}},
series = {Lecture Notes in Computer Science},
volume = {5126},
pages = {336--347},
publisher = {Springer},
year = {2008}
}
@inproceedings{DBLP:conf/lpar/McLaughlinP08,
author = {Sean McLaughlin and
Frank Pfenning},
title = {Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional
Logic},
booktitle = {{LPAR}},
series = {Lecture Notes in Computer Science},
volume = {5330},
pages = {174--181},
publisher = {Springer},
year = {2008}
}
@inproceedings{DBLP:conf/icfp/Pfenning07,
author = {Frank Pfenning},
title = {Subtyping and intersection types revisited},
booktitle = {{ICFP}},
pages = {219},
publisher = {{ACM}},
year = {2007}
}
@inproceedings{DBLP:conf/icra/SaranliP07,
author = {Uluc Saranli and
Frank Pfenning},
title = {Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning
Problems},
booktitle = {{ICRA}},
pages = {3705--3710},
publisher = {{IEEE}},
year = {2007}
}
@inproceedings{DBLP:conf/ndss/BowersBGPR07,
author = {Kevin D. Bowers and
Lujo Bauer and
Deepak Garg and
Frank Pfenning and
Michael K. Reiter},
title = {Consumable Credentials in Linear-Logic-Based Access-Control Systems},
booktitle = {{NDSS}},
publisher = {The Internet Society},
year = {2007}
}
@inproceedings{DBLP:conf/rta/Pfenning07,
author = {Frank Pfenning},
title = {On a Logical Foundation for Explicit Substitutions},
booktitle = {{RTA}},
series = {Lecture Notes in Computer Science},
volume = {4533},
pages = {19},
publisher = {Springer},
year = {2007}
}
@inproceedings{DBLP:conf/tlca/Pfenning07,
author = {Frank Pfenning},
title = {On a Logical Foundation for Explicit Substitutions},
booktitle = {{TLCA}},
series = {Lecture Notes in Computer Science},
volume = {4583},
pages = {1},
publisher = {Springer},
year = {2007}
}
@inproceedings{DBLP:journals/entcs/ReedP09,
author = {Jason Reed and
Frank Pfenning},
title = {Intuitionistic Letcc via Labelled Deduction},
booktitle = {{M4M}},
series = {Electronic Notes in Theoretical Computer Science},
volume = {231},
pages = {91--111},
publisher = {Elsevier},
year = {2007}
}
@inproceedings{DBLP:journals/entcs/LovasP08,
author = {William Lovas and
Frank Pfenning},
title = {A Bidirectional Refinement Type System for {LF}},
booktitle = {LFMTP@CADE},
series = {Electronic Notes in Theoretical Computer Science},
volume = {196},
pages = {113--128},
publisher = {Elsevier},
year = {2007}
}
@proceedings{DBLP:conf/cade/2007,
editor = {Frank Pfenning},
title = {Automated Deduction - CADE-21, 21st International Conference on Automated
Deduction, Bremen, Germany, July 17-20, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4603},
publisher = {Springer},
year = {2007}
}
@inproceedings{DBLP:conf/cade/ChaudhuriPP06,
author = {Kaustuv Chaudhuri and
Frank Pfenning and
Greg Price},
title = {A Logical Characterization of Forward and Backward Chaining in the
Inverse Method},
booktitle = {{IJCAR}},
series = {Lecture Notes in Computer Science},
volume = {4130},
pages = {97--111},
publisher = {Springer},
year = {2006}
}
@inproceedings{DBLP:conf/csfw/GargP06,
author = {Deepak Garg and
Frank Pfenning},
title = {Non-Interference in Constructive Authorization Logic},
booktitle = {{CSFW}},
pages = {283--296},
publisher = {{IEEE} Computer Society},
year = {2006}
}
@inproceedings{DBLP:conf/esorics/GargBBPR06,
author = {Deepak Garg and
Lujo Bauer and
Kevin D. Bowers and
Frank Pfenning and
Michael K. Reiter},
title = {A Linear Logic of Authorization and Knowledge},
booktitle = {{ESORICS}},
series = {Lecture Notes in Computer Science},
volume = {4189},
pages = {297--312},
publisher = {Springer},
year = {2006}
}
@proceedings{DBLP:conf/rta/2006,
editor = {Frank Pfenning},
title = {Term Rewriting and Applications, 17th International Conference, {RTA}
2006, Seattle, WA, USA, August 12-14, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4098},
publisher = {Springer},
year = {2006}
}
@article{DBLP:journals/jfp/CraryKP05,
author = {Karl Crary and
Aleksey Kliger and
Frank Pfenning},
title = {A monadic analysis of information flow security with mutable state},
journal = {J. Funct. Program.},
volume = {15},
number = {2},
pages = {249--291},
year = {2005}
}
@article{DBLP:journals/jfp/NanevskiP05,
author = {Aleksandar Nanevski and
Frank Pfenning},
title = {Staged computation with names and necessity},
journal = {J. Funct. Program.},
volume = {15},
number = {5},
pages = {893--939},
year = {2005}
}
@article{DBLP:journals/tocl/HarperP05,
author = {Robert Harper and
Frank Pfenning},
title = {On equivalence and canonical forms in the {LF} type theory},
journal = {{ACM} Trans. Comput. Log.},
volume = {6},
number = {1},
pages = {61--101},
year = {2005}
}
@inproceedings{DBLP:conf/cade/ChaudhuriP05,
author = {Kaustuv Chaudhuri and
Frank Pfenning},
title = {A Focusing Inverse Method Theorem Prover for First-Order Linear Logic},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {3632},
pages = {69--83},
publisher = {Springer},
year = {2005}
}
@inproceedings{DBLP:conf/concur/GargP05,
author = {Deepak Garg and
Frank Pfenning},
title = {Type-Directed Concurrency},
booktitle = {{CONCUR}},
series = {Lecture Notes in Computer Science},
volume = {3653},
pages = {6--20},
publisher = {Springer},
year = {2005}
}
@inproceedings{DBLP:conf/csl/ChaudhuriP05,
author = {Kaustuv Chaudhuri and
Frank Pfenning},
title = {Focusing the Inverse Method for Linear Logic},
booktitle = {{CSL}},
series = {Lecture Notes in Computer Science},
volume = {3634},
pages = {200--215},
publisher = {Springer},
year = {2005}
}
@inproceedings{DBLP:conf/icfp/Pfenning05,
author = {Frank Pfenning},
title = {Towards a type theory of contexts},
booktitle = {{MERLIN}},
pages = {1},
publisher = {{ACM}},
year = {2005}
}
@inproceedings{DBLP:conf/popl/ParkPT05,
author = {Sungwoo Park and
Frank Pfenning and
Sebastian Thrun},
title = {A probabilistic language based upon sampling functions},
booktitle = {{POPL}},
pages = {171--182},
publisher = {{ACM}},
year = {2005}
}
@inproceedings{DBLP:conf/ppdp/LopezPPW05,
author = {Pablo L{\'{o}}pez and
Frank Pfenning and
Jeff Polakow and
Kevin Watkins},
title = {Monadic concurrent linear logic programming},
booktitle = {{PPDP}},
pages = {35--46},
publisher = {{ACM}},
year = {2005}
}
@article{DBLP:journals/jar/AndrewsBPBIX04,
author = {Peter B. Andrews and
Chad E. Brown and
Frank Pfenning and
Matthew Bishop and
Sunil Issar and
Hongwei Xi},
title = {{ETPS:} {A} System to Help Students Write Formal Proofs},
journal = {J. Autom. Reason.},
volume = {32},
number = {1},
pages = {75--92},
year = {2004}
}
@inproceedings{DBLP:conf/aplas/Pfenning04,
author = {Frank Pfenning},
title = {Substructural Operational Semantics and Linear Destination-Passing
Style (Invited Talk)},
booktitle = {{APLAS}},
series = {Lecture Notes in Computer Science},
volume = {3302},
pages = {196},
publisher = {Springer},
year = {2004}
}
@inproceedings{DBLP:conf/lics/VIICHP04,
author = {Tom Murphy VII and
Karl Crary and
Robert Harper and
Frank Pfenning},
title = {A Symmetric Modal Lambda Calculus for Distributed Computing},
booktitle = {{LICS}},
pages = {286--295},
publisher = {{IEEE} Computer Society},
year = {2004}
}
@inproceedings{DBLP:conf/popl/DunfieldP04,
author = {Jana Dunfield and
Frank Pfenning},
title = {Tridirectional typechecking},
booktitle = {{POPL}},
pages = {281--292},
publisher = {{ACM}},
year = {2004}
}
@inproceedings{DBLP:conf/tphol/AndersonP04,
author = {Penny Anderson and
Frank Pfenning},
title = {Verifying Uniqueness in a Logical Framework},
booktitle = {TPHOLs},
series = {Lecture Notes in Computer Science},
volume = {3223},
pages = {18--33},
publisher = {Springer},
year = {2004}
}
@inproceedings{DBLP:journals/entcs/WatkinsCPW08,
author = {Kevin Watkins and
Iliano Cervesato and
Frank Pfenning and
David Walker},
title = {Specifying Properties of Concurrent Computations in {CLF}},
booktitle = {LFM@IJCAR},
series = {Electronic Notes in Theoretical Computer Science},
volume = {199},
pages = {67--87},
publisher = {Elsevier},
year = {2004}
}
@article{DBLP:journals/logcom/CervesatoP03,
author = {Iliano Cervesato and
Frank Pfenning},
title = {A Linear Spine Calculus},
journal = {J. Log. Comput.},
volume = {13},
number = {5},
pages = {639--688},
year = {2003}
}
@article{DBLP:journals/tcs/ColbyCHLP03,
author = {Christopher Colby and
Karl Crary and
Robert Harper and
Peter Lee and
Frank Pfenning},
title = {Automated techniques for provably safe mobile code},
journal = {Theor. Comput. Sci.},
volume = {290},
number = {2},
pages = {1175--1199},
year = {2003}
}
@article{DBLP:journals/tocl/MomiglianoP03,
author = {Alberto Momigliano and
Frank Pfenning},
title = {Higher-order pattern complement and the strict lambda-calculus},
journal = {{ACM} Trans. Comput. Log.},
volume = {4},
number = {4},
pages = {493--529},
year = {2003}
}
@inproceedings{DBLP:conf/cade/PientkaP03,
author = {Brigitte Pientka and
Frank Pfenning},
title = {Optimizing Higher-Order Pattern Unification},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {2741},
pages = {473--487},
publisher = {Springer},
year = {2003}
}
@inproceedings{DBLP:conf/fossacs/DunfieldP03,
author = {Jana Dunfield and
Frank Pfenning},
title = {Type Assignment for Intersections and Unions in Call-by-Value Languages},
booktitle = {FoSSaCS},
series = {Lecture Notes in Computer Science},
volume = {2620},
pages = {250--266},
publisher = {Springer},
year = {2003}
}
@inproceedings{DBLP:conf/icfp/NanevskiPP03,
author = {Aleksandar Nanevski and
Brigitte Pientka and
Frank Pfenning},
title = {A modal foundation for meta-variables},
booktitle = {{MERLIN}},
publisher = {{ACM}},
year = {2003}
}
@inproceedings{DBLP:conf/ijcai/ThrunGPBSL03,
author = {Sebastian Thrun and
Geoffrey J. Gordon and
Frank Pfenning and
Mary Berna and
Brennan Sellner and
Brad Lisien},
title = {A Learning Algorithm for Localizing People Based on Wireless Signal
Strength that Uses Labeled and Unlabeled Data},
booktitle = {{IJCAI}},
pages = {1427--1428},
publisher = {Morgan Kaufmann},
year = {2003}
}
@inproceedings{DBLP:conf/popl/PetersenHCP03,
author = {Leaf Petersen and
Robert Harper and
Karl Crary and
Frank Pfenning},
title = {A type theory for memory allocation and data layout},
booktitle = {{POPL}},
pages = {172--184},
publisher = {{ACM}},
year = {2003}
}
@inproceedings{DBLP:conf/tphol/SchurmannP03,
author = {Carsten Sch{\"{u}}rmann and
Frank Pfenning},
title = {A Coverage Checking Algorithm for {LF}},
booktitle = {TPHOLs},
series = {Lecture Notes in Computer Science},
volume = {2758},
pages = {120--135},
publisher = {Springer},
year = {2003}
}
@inproceedings{DBLP:conf/types/WatkinsCPW03,
author = {Kevin Watkins and
Iliano Cervesato and
Frank Pfenning and
David Walker},
title = {A Concurrent Logical Framework: The Propositional Fragment},
booktitle = {{TYPES}},
series = {Lecture Notes in Computer Science},
volume = {3085},
pages = {355--377},
publisher = {Springer},
year = {2003}
}
@proceedings{DBLP:conf/gpce/2003,
editor = {Frank Pfenning and
Yannis Smaragdakis},
title = {Generative Programming and Component Engineering, Second International
Conference, {GPCE} 2003, Erfurt, Germany, September 22-25, 2003, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2830},
publisher = {Springer},
year = {2003}
}
@article{DBLP:journals/iandc/CervesatoP02,
author = {Iliano Cervesato and
Frank Pfenning},
title = {A Linear Logical Framework},
journal = {Inf. Comput.},
volume = {179},
number = {1},
pages = {19--75},
year = {2002}
}
@article{DBLP:journals/tocl/AbadiLP02,
author = {Mart{\'{\i}}n Abadi and
Leonid Libkin and
Frank Pfenning},
title = {Editorial},
journal = {{ACM} Trans. Comput. Log.},
volume = {3},
number = {3},
pages = {335--335},
year = {2002}
}
@inproceedings{DBLP:conf/grid/ChangCDHLVP02,
author = {Bor{-}Yuh Evan Chang and
Karl Crary and
Margaret DeLap and
Robert Harper and
Jason Liszka and
Tom Murphy VII and
Frank Pfenning},
title = {Trustless Grid Computing in ConCert},
booktitle = {{GRID}},
series = {Lecture Notes in Computer Science},
volume = {2536},
pages = {112--125},
publisher = {Springer},
year = {2002}
}
@inproceedings{DBLP:journals/entcs/Pfenning02,
author = {Frank Pfenning},
title = {Preface},
booktitle = {{LFM}},
series = {Electronic Notes in Theoretical Computer Science},
volume = {70},
number = {2},
pages = {146},
publisher = {Elsevier},
year = {2002}
}
@inproceedings{DBLP:journals/entcs/Pfenning02a,
author = {Frank Pfenning},
title = {Invited talk: Tri-Directional Type Checking},
booktitle = {{ITRS}},
series = {Electronic Notes in Theoretical Computer Science},
volume = {70},
number = {1},
publisher = {Elsevier},
year = {2002}
}
@proceedings{DBLP:conf/lfm/2002,
editor = {Frank Pfenning},
title = {International Workshop on Logical Frameworks and Meta-Languages, {LFM}
2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002},
series = {Electronic Notes in Theoretical Computer Science},
volume = {70},
number = {2},
publisher = {Elsevier},
year = {2002}
}
@article{DBLP:journals/jacm/DaviesP01,
author = {Rowan Davies and
Frank Pfenning},
title = {A modal analysis of staged computation},
journal = {J. {ACM}},
volume = {48},
number = {3},
pages = {555--604},
year = {2001}
}
@article{DBLP:journals/mscs/PfenningD01,
author = {Frank Pfenning and
Rowan Davies},
title = {A judgmental reconstruction of modal logic},
journal = {Math. Struct. Comput. Sci.},
volume = {11},
number = {4},
pages = {511--540},
year = {2001}
}
@article{DBLP:journals/tcs/SchurmannDP01,
author = {Carsten Sch{\"{u}}rmann and
Jo{\"{e}}lle Despeyroux and
Frank Pfenning},
title = {Primitive recursion for higher-order abstract syntax},
journal = {Theor. Comput. Sci.},
volume = {266},
number = {1-2},
pages = {1--57},
year = {2001}
}
@inproceedings{DBLP:conf/lics/Pfenning01,
author = {Frank Pfenning},
title = {Intensionality, Extensionality, and Proof Irrelevance in Modal Type
Theory},
booktitle = {{LICS}},
pages = {221--230},
publisher = {{IEEE} Computer Society},
year = {2001}
}
@incollection{DBLP:books/el/RV01/Pfenning01,
author = {Frank Pfenning},
title = {Logical Frameworks},
booktitle = {Handbook of Automated Reasoning},
pages = {1063--1147},
publisher = {Elsevier and {MIT} Press},
year = {2001}
}
@article{DBLP:journals/corr/cs-LO-0109072,
author = {Alberto Momigliano and
Frank Pfenning},
title = {Higher-Order Pattern Complement and the Strict Lambda-Calculus},
journal = {CoRR},
volume = {cs.LO/0109072},
year = {2001}
}
@article{DBLP:journals/corr/cs-LO-0110028,
author = {Robert Harper and
Frank Pfenning},
title = {On Equivalence and Canonical Forms in the {LF} Type Theory},
journal = {CoRR},
volume = {cs.LO/0110028},
year = {2001}
}
@article{DBLP:journals/amai/GramlichKP00,
author = {Bernhard Gramlich and
H{\'{e}}l{\`{e}}ne Kirchner and
Frank Pfenning},
title = {Editorial: Strategies in Automated Deduction},
journal = {Ann. Math. Artif. Intell.},
volume = {29},
number = {1-4},
year = {2000}
}
@article{DBLP:journals/iandc/Pfenning00,
author = {Frank Pfenning},
title = {Structural Cut Elimination: I. Intuitionistic and Classical Logic},
journal = {Inf. Comput.},
volume = {157},
number = {1-2},
pages = {84--141},
year = {2000}
}
@article{DBLP:journals/tcs/CervesatoHP00,
author = {Iliano Cervesato and
Joshua S. Hodas and
Frank Pfenning},
title = {Efficient resource management for linear logic proof search},
journal = {Theor. Comput. Sci.},
volume = {232},
number = {1-2},
pages = {133--163},
year = {2000}
}
@inproceedings{DBLP:conf/icfp/DaviesP00,
author = {Rowan Davies and
Frank Pfenning},
title = {Intersection types and computational effects},
booktitle = {{ICFP}},
pages = {198--208},
publisher = {{ACM}},
year = {2000}
}
@inproceedings{DBLP:conf/pepm/Pfenning00,
author = {Frank Pfenning},
title = {On the Logical Foundations of Staged Computation (Abstract of Invited
Talk)},
booktitle = {{PEPM}},
pages = {33},
publisher = {{ACM}},
year = {2000}
}
@inproceedings{DBLP:conf/saig/Pfenning00,
author = {Frank Pfenning},
title = {Reasoning about Staged Computation},
booktitle = {{SAIG}},
series = {Lecture Notes in Computer Science},
volume = {1924},
pages = {5--6},
publisher = {Springer},
year = {2000}
}
@proceedings{DBLP:conf/ppdp/2000,
editor = {Maurizio Gabbrielli and
Frank Pfenning},
title = {Proceedings of the 2nd international {ACM} {SIGPLAN} conference on
on Principles and practice of declarative programming, Montreal, Canada,
September 20-23, 2000},
publisher = {{ACM}},
year = {2000}
}
@inproceedings{DBLP:conf/agp/MomiglianoP99,
author = {Alberto Momigliano and
Frank Pfenning},
title = {The Relative Complement Problem for Higher-Order Patterns},
booktitle = {{APPIA-GULP-PRODE}},
pages = {497--512},
year = {1999}
}
@inproceedings{DBLP:conf/cade/PfenningS99,
author = {Frank Pfenning and
Carsten Sch{\"{u}}rmann},
title = {System Description: Twelf - {A} Meta-Logical Framework for Deductive
Systems},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {1632},
pages = {202--206},
publisher = {Springer},
year = {1999}
}
@inproceedings{DBLP:conf/iclp/MomiglianoP99,
author = {Alberto Momigliano and
Frank Pfenning},
title = {The Relative Complement Problem for Higher-Order Patterns},
booktitle = {{ICLP}},
pages = {380--394},
publisher = {{MIT} Press},
year = {1999}
}
@inproceedings{DBLP:conf/popl/XiP99,
author = {Hongwei Xi and
Frank Pfenning},
title = {Dependent Types in Practical Programming},
booktitle = {{POPL}},
pages = {214--227},
publisher = {{ACM}},
year = {1999}
}
@inproceedings{DBLP:conf/ppdp/Pfenning99,
author = {Frank Pfenning},
title = {Logical and Meta-Logical Frameworks (Abstract)},
booktitle = {{PPDP}},
series = {Lecture Notes in Computer Science},
volume = {1702},
pages = {206},
publisher = {Springer},
year = {1999}
}
@inproceedings{DBLP:conf/tlca/PolakowP99,
author = {Jeff Polakow and
Frank Pfenning},
title = {Natural Deduction for Intuitionistic Non-communicative Linear Logic},
booktitle = {{TLCA}},
series = {Lecture Notes in Computer Science},
volume = {1581},
pages = {295--309},
publisher = {Springer},
year = {1999}
}
@inproceedings{DBLP:journals/entcs/DanvyDP99,
author = {Olivier Danvy and
Belmina Dzafic and
Frank Pfenning},
title = {On proving syntactic properties of {CPS} programs},
booktitle = {{HOOTS}},
series = {Electronic Notes in Theoretical Computer Science},
volume = {26},
pages = {21--33},
publisher = {Elsevier},
year = {1999}
}
@inproceedings{DBLP:journals/entcs/PolokowP99,
author = {J. Polokow and
Frank Pfenning},
title = {Relating Natural Deduction and Sequent Calculus for Intuitionistic
Non-Commutative Linear Logic},
booktitle = {{MFPS}},
series = {Electronic Notes in Theoretical Computer Science},
volume = {20},
pages = {449--466},
publisher = {Elsevier},
year = {1999}
}
@article{DBLP:journals/csur/WicklineLPD98,
author = {Philip Wickline and
Peter Lee and
Frank Pfenning and
Rowan Davies},
title = {Modal Types as Staging Specifications for Run-Time Code Generation},
journal = {{ACM} Comput. Surv.},
volume = {30},
number = {3es},
pages = {8},
year = {1998}
}
@article{DBLP:journals/logcom/HarperP98,
author = {Robert Harper and
Frank Pfenning},
title = {A Module System for a Programming Language Based on the {LF} Logical
Framework},
journal = {J. Log. Comput.},
volume = {8},
number = {1},
pages = {5--31},
year = {1998}
}
@article{DBLP:journals/sLogica/SiegP98,
author = {Wilfried Sieg and
Frank Pfenning},
title = {Note by the Guest Editors},
journal = {Stud Logica},
volume = {60},
number = {1},
pages = {1},
year = {1998}
}
@inproceedings{DBLP:conf/cade/Pfenning98,
author = {Frank Pfenning},
title = {Reasoning About Deductions in Linear Logic (Abstract of Invited Talk)},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {1421},
pages = {1--2},
publisher = {Springer},
year = {1998}
}
@inproceedings{DBLP:conf/cade/SchurmannP98,
author = {Carsten Sch{\"{u}}rmann and
Frank Pfenning},
title = {Automated Theorem Proving in a Simple Meta-Logic for {LF}},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {1421},
pages = {286--300},
publisher = {Springer},
year = {1998}
}
@inproceedings{DBLP:conf/pldi/WicklineLP98,
author = {Philip Wickline and
Peter Lee and
Frank Pfenning},
title = {Run-time Code Generation and Modal-ML},
booktitle = {{PLDI}},
pages = {224--235},
publisher = {{ACM}},
year = {1998}
}
@inproceedings{DBLP:conf/pldi/XiP98,
author = {Hongwei Xi and
Frank Pfenning},
title = {Eliminating Array Bound Checking Through Dependent Types},
booktitle = {{PLDI}},
pages = {249--257},
publisher = {{ACM}},
year = {1998}
}
@inproceedings{DBLP:conf/types/PfenningS98,
author = {Frank Pfenning and
Carsten Sch{\"{u}}rmann},
title = {Algorithms for Equality and Unification in the Presence of Notational
Definitions},
booktitle = {{TYPES}},
series = {Lecture Notes in Computer Science},
volume = {1657},
pages = {179--193},
publisher = {Springer},
year = {1998}
}
@inproceedings{DBLP:journals/entcs/PfenningS98,
author = {Frank Pfenning and
Carsten Sch{\"{u}}rmann},
title = {Algorithms for Equality and Unification in the Presence of Notational
Definitions},
booktitle = {Proof Search in Type-Theoretic Languages@CADE},
series = {Electronic Notes in Theoretical Computer Science},
volume = {17},
pages = {1--13},
publisher = {Elsevier},
year = {1998}
}
@article{DBLP:journals/jsyml/NarendranPS97,
author = {Paliath Narendran and
Frank Pfenning and
Richard Statman},
title = {On the Unification Problem for Cartesian Closed Categories},
journal = {J. Symb. Log.},
volume = {62},
number = {2},
pages = {636--647},
year = {1997}
}
@inproceedings{DBLP:conf/lics/CervesatoP97,
author = {Iliano Cervesato and
Frank Pfenning},
title = {Linear Higher-Order Pre-Unification},
booktitle = {{LICS}},
pages = {422--433},
publisher = {{IEEE} Computer Society},
year = {1997}
}
@inproceedings{DBLP:conf/tlca/DespeyrouxPS97,
author = {Jo{\"{e}}lle Despeyroux and
Frank Pfenning and
Carsten Sch{\"{u}}rmann},
title = {Primitive Recursion for Higher-Order Abstract Syntax},
booktitle = {{TLCA}},
series = {Lecture Notes in Computer Science},
volume = {1210},
pages = {147--163},
publisher = {Springer},
year = {1997}
}
@article{DBLP:journals/jar/AndrewsBINPX96,
author = {Peter B. Andrews and
Matthew Bishop and
Sunil Issar and
Dan Nesmith and
Frank Pfenning and
Hongwei Xi},
title = {{TPS:} {A} Theorem-Proving System for Classical Type Theory},
journal = {J. Autom. Reason.},
volume = {16},
number = {3},
pages = {321--353},
year = {1996}
}
@inproceedings{DBLP:conf/caap/Pfenning96,
author = {Frank Pfenning},
title = {The Practice of Logical Frameworks},
booktitle = {{CAAP}},
series = {Lecture Notes in Computer Science},
volume = {1059},
pages = {119--134},
publisher = {Springer},
year = {1996}
}
@inproceedings{DBLP:conf/elp/CervesatoHP96,
author = {Iliano Cervesato and
Joshua S. Hodas and
Frank Pfenning},
title = {Efficient Resource Management for Linear Logic Proof Search},
booktitle = {{ELP}},
series = {Lecture Notes in Computer Science},
volume = {1050},
pages = {67--81},
publisher = {Springer},
year = {1996}
}
@inproceedings{DBLP:conf/esop/RohwedderP96,
author = {Ekkehard Rohwedder and
Frank Pfenning},
title = {Mode and Termination Checking for Higher-Order Logic Programs},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {1058},
pages = {296--310},
publisher = {Springer},
year = {1996}
}
@inproceedings{DBLP:conf/iclp/DowekHKP96,
author = {Gilles Dowek and
Th{\'{e}}r{\`{e}}se Hardin and
Claude Kirchner and
Frank Pfenning},
title = {Unification via Explicit Substitutions: The Case of Higher-Order Patterns},
booktitle = {{JICSLP}},
pages = {259--273},
publisher = {{MIT} Press},
year = {1996}
}
@inproceedings{DBLP:conf/lics/CervesatoP96,
author = {Iliano Cervesato and
Frank Pfenning},
title = {A Linear Logical Framework},
booktitle = {{LICS}},
pages = {264--275},
publisher = {{IEEE} Computer Society},
year = {1996}
}
@inproceedings{DBLP:conf/popl/DaviesP96,
author = {Rowan Davies and
Frank Pfenning},
title = {A Modal Analysis of Staged Computation},
booktitle = {{POPL}},
pages = {258--270},
publisher = {{ACM} Press},
year = {1996}
}
@inproceedings{DBLP:conf/lics/Pfenning95,
author = {Frank Pfenning},
title = {Structural Cut Elimination},
booktitle = {{LICS}},
pages = {156--166},
publisher = {{IEEE} Computer Society},
year = {1995}
}
@inproceedings{DBLP:journals/entcs/PfenningW95,
author = {Frank Pfenning and
Hao{-}Chi Wong},
title = {On a modal lambda calculus for {S4}},
booktitle = {{MFPS}},
series = {Electronic Notes in Theoretical Computer Science},
volume = {1},
pages = {515--534},
publisher = {Elsevier},
year = {1995}
}
@inproceedings{DBLP:conf/cade/Pfenning94,
author = {Frank Pfenning},
title = {Elf: {A} Meta-Language for Deductive Systems (System Descrition)},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {814},
pages = {811--815},
publisher = {Springer},
year = {1994}
}
@proceedings{DBLP:conf/lpar/1994,
editor = {Frank Pfenning},
title = {Logic Programming and Automated Reasoning, 5th International Conference,
LPAR'94, Kiev, Ukraine, July 16-22, 1994, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {822},
publisher = {Springer},
year = {1994}
}
@article{DBLP:journals/fuin/Pfenning93,
author = {Frank Pfenning},
title = {On the Undecidability of Partial Polymorphic Type Reconstruction},
journal = {Fundam. Informaticae},
volume = {19},
number = {1/2},
pages = {185--199},
year = {1993}
}
@inproceedings{DBLP:conf/lics/NarendranPS93,
author = {Paliath Narendran and
Frank Pfenning and
Richard Statman},
title = {On the Unification Problem for Cartesian Closed Categories},
booktitle = {{LICS}},
pages = {57--63},
publisher = {{IEEE} Computer Society},
year = {1993}
}
@inproceedings{DBLP:conf/ppcp/MichaylovP93,
author = {Spiro Michaylov and
Frank Pfenning},
title = {Higher-Order Logic Programming as Constraint Logic Programming},
booktitle = {{PPCP}},
pages = {210--218},
year = {1993}
}
@inproceedings{DBLP:conf/slp/KohlhaseP93,
author = {Michael Kohlhase and
Frank Pfenning},
title = {Unification in a Lambda-Calculus with Intersection Types},
booktitle = {{ILPS}},
pages = {488--505},
publisher = {{MIT} Press},
year = {1993}
}
@inproceedings{DBLP:conf/tphol/AndrewsBINPX93,
author = {Peter B. Andrews and
Matthew Bishop and
Sunil Issar and
Dan Nesmith and
Frank Pfenning and
Hongwei Xi},
title = {{TPS:} An Interactive and Automatic Tool for Proving Theorems of Type
Theory},
booktitle = {{HUG}},
series = {Lecture Notes in Computer Science},
volume = {780},
pages = {366--370},
publisher = {Springer},
year = {1993}
}
@article{DBLP:journals/ml/DietzenP92,
author = {Scott Dietzen and
Frank Pfenning},
title = {Higher-Order and Modal Logic as a Framework for Explanation-Based
Generalization},
journal = {Mach. Learn.},
volume = {9},
pages = {23--55},
year = {1992}
}
@inproceedings{DBLP:conf/cade/PfenningR92,
author = {Frank Pfenning and
Ekkehard Rohwedder},
title = {Implementing the Meta-Theory of Deductive Systems},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {607},
pages = {537--551},
publisher = {Springer},
year = {1992}
}
@inproceedings{DBLP:conf/lics/PfenningH92,
author = {John Hannan and
Frank Pfenning},
title = {Compiler Verification in {LF}},
booktitle = {{LICS}},
pages = {407--418},
publisher = {{IEEE} Computer Society},
year = {1992}
}
@incollection{DBLP:books/mit/pfenning92/NadathurP92,
author = {Gopalan Nadathur and
Frank Pfenning},
title = {The Type System of a Higher-Order Logic Programming Language},
booktitle = {Types in Logic Programming},
pages = {245--283},
publisher = {The {MIT} Press},
year = {1992}
}
@incollection{DBLP:books/mit/pfenning92/Pfenning92,
author = {Frank Pfenning},
title = {Dependent Types in Logic Programming},
booktitle = {Types in Logic Programming},
pages = {285--311},
publisher = {The {MIT} Press},
year = {1992}
}
@book{DBLP:books/mit/pfenning92/P1992,
editor = {Frank Pfenning},
title = {Types in Logic Programming},
publisher = {The {MIT} Press},
year = {1992}
}
@article{DBLP:journals/apal/MillerNPS91,
author = {Dale Miller and
Gopalan Nadathur and
Frank Pfenning and
Andre Scedrov},
title = {Uniform Proofs as a Foundation for Logic Programming},
journal = {Ann. Pure Appl. Log.},
volume = {51},
number = {1-2},
pages = {125--157},
year = {1991}
}
@article{DBLP:journals/tcs/PfenningL91,
author = {Frank Pfenning and
Peter Lee},
title = {Metacircularity in the Polymorphic lambda-Calculus},
journal = {Theor. Comput. Sci.},
volume = {89},
number = {1},
pages = {137--159},
year = {1991}
}
@inproceedings{DBLP:conf/elp/MichaylovP91,
author = {Spiro Michaylov and
Frank Pfenning},
title = {Natural Semantics and Some of Its Meta-Theory in Elf},
booktitle = {{ELP}},
series = {Lecture Notes in Computer Science},
volume = {596},
pages = {299--344},
publisher = {Springer},
year = {1991}
}
@inproceedings{DBLP:conf/lics/Pfenning91,
author = {Frank Pfenning},
title = {Unification and Anti-Unification in the Calculus of Constructions},
booktitle = {{LICS}},
pages = {74--85},
publisher = {{IEEE} Computer Society},
year = {1991}
}
@inproceedings{DBLP:conf/pepm/MichaylovP91,
author = {Spiro Michaylov and
Frank Pfenning},
title = {Compiling the Polymorphic Lambda-Calculus},
booktitle = {{PEPM}},
pages = {285--296},
publisher = {{ACM}},
year = {1991}
}
@inproceedings{DBLP:conf/pldi/FreemanP91,
author = {Timothy S. Freeman and
Frank Pfenning},
title = {Refinement Types for {ML}},
booktitle = {{PLDI}},
pages = {268--277},
publisher = {{ACM}},
year = {1991}
}
@inproceedings{DBLP:conf/slp/DietzenP91,
author = {Scott Dietzen and
Frank Pfenning},
title = {A Declarative Alternative to "Assert" in Logic Programming},
booktitle = {{ISLP}},
pages = {372--386},
publisher = {{MIT} Press},
year = {1991}
}
@inproceedings{DBLP:conf/cade/PfenningN90,
author = {Frank Pfenning and
Dan Nesmith},
title = {Presenting Intuitive Deductions via Symmetric Simplification},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {449},
pages = {336--350},
publisher = {Springer},
year = {1990}
}
@inproceedings{DBLP:conf/cade/AndrewsINP90,
author = {Peter B. Andrews and
Sunil Issar and
Dan Nesmith and
Frank Pfenning},
title = {The {TPS} Theorem Proving System},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {449},
pages = {641--642},
publisher = {Springer},
year = {1990}
}
@inproceedings{DBLP:conf/cade/FeltyGMP90,
author = {Amy P. Felty and
Elsa L. Gunter and
Dale Miller and
Frank Pfenning},
title = {Tutorial on Lambda-Prolog},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {449},
pages = {682},
publisher = {Springer},
year = {1990}
}
@inproceedings{DBLP:conf/iclp/Pfenning90,
author = {Frank Pfenning},
title = {Types in Logic Programming},
booktitle = {{ICLP}},
pages = {786},
publisher = {{MIT} Press},
year = {1990}
}
@inproceedings{DBLP:conf/icml/DietzenP89,
author = {Scott Dietzen and
Frank Pfenning},
title = {Higher-Order and Modal Logic as a Framework for Explanation-Based
Generalization},
booktitle = {{ML}},
pages = {447--449},
publisher = {Morgan Kaufmann},
year = {1989}
}
@inproceedings{DBLP:conf/lics/Pfenning89,
author = {Frank Pfenning},
title = {Elf: {A} Language for Logic Definition and Verified Metaprogramming},
booktitle = {{LICS}},
pages = {313--322},
publisher = {{IEEE} Computer Society},
year = {1989}
}
@inproceedings{DBLP:conf/mfps/PfenningP89,
author = {Frank Pfenning and
Christine Paulin{-}Mohring},
title = {Inductively Defined Types in the Calculus of Constructions},
booktitle = {Mathematical Foundations of Programming Semantics},
series = {Lecture Notes in Computer Science},
volume = {442},
pages = {209--228},
publisher = {Springer},
year = {1989}
}
@inproceedings{DBLP:conf/tapsoft/PfenningL89,
author = {Frank Pfenning and
Peter Lee},
title = {{LEAP:} {A} Language with Eval And Polymorphism},
booktitle = {TAPSOFT, Vol.2},
series = {Lecture Notes in Computer Science},
volume = {352},
pages = {345--359},
publisher = {Springer},
year = {1989}
}
@inproceedings{DBLP:conf/cade/Pfenning88,
author = {Frank Pfenning},
title = {Single Axioms in the Implicational Propositional Calculus},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {310},
pages = {710--713},
publisher = {Springer},
year = {1988}
}
@inproceedings{DBLP:conf/cade/AndrewsINP88,
author = {Peter B. Andrews and
Sunil Issar and
Daniel Nesmith and
Frank Pfenning},
title = {The {TPS} Theorem Proving System},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {310},
pages = {760--761},
publisher = {Springer},
year = {1988}
}
@inproceedings{DBLP:conf/lfp/Pfenning88,
author = {Frank Pfenning},
title = {Partial Polymorphic Type Inference and Higher-Order Unification},
booktitle = {{LISP} and Functional Programming},
pages = {153--163},
publisher = {{ACM}},
year = {1988}
}
@inproceedings{DBLP:conf/pldi/PfenningE88,
author = {Frank Pfenning and
Conal Elliott},
title = {Higher-Order Abstract Syntax},
booktitle = {{PLDI}},
pages = {199--208},
publisher = {{ACM}},
year = {1988}
}
@inproceedings{DBLP:conf/sde/LeePRS88,
author = {Peter Lee and
Frank Pfenning and
Gene Rollins and
William L. Scherlis},
title = {The Ergo Support System: An Integrated Set of Tools for Prototyping
Integrated Environments},
booktitle = {Software Development Environments {(SDE)}},
pages = {25--34},
publisher = {{ACM}},
year = {1988}
}
@inproceedings{DBLP:conf/sde/NordP88,
author = {Robert L. Nord and
Frank Pfenning},
title = {The Ergo Attribute System},
booktitle = {Software Development Environments {(SDE)}},
pages = {110--120},
publisher = {{ACM}},
year = {1988}
}
@inproceedings{DBLP:conf/cade/AndrewsPIK86,
author = {Peter B. Andrews and
Frank Pfenning and
Sunil Issar and
Carl P. Klapper},
title = {The {TPS} Theorem Proving System},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {230},
pages = {663--664},
publisher = {Springer},
year = {1986}
}
@inproceedings{DBLP:conf/cade/Pfenning84,
author = {Frank Pfenning},
title = {Analytic and Non-analytic Proofs},
booktitle = {{CADE}},
series = {Lecture Notes in Computer Science},
volume = {170},
pages = {394--413},
publisher = {Springer},
year = {1984}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-05-02 23:42 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
