BibSLEIGH — Frank

Travelled to:

1 × Brazil
1 × Denmark
1 × Finland
1 × Iceland
1 × Israel
1 × Portugal
1 × Sweden
1 × The Netherlands
2 × Poland
2 × United Kingdom
23 × USA
3 × Estonia
3 × Germany
4 × Italy
6 × Canada
6 × France

Collaborated with:

∅ B.Toninho L.Caires R.J.Simmons K.Chaudhuri C.Schürmann J.Dunfield R.Davies H.Xi I.Cervesato E.Rohwedder S.Dietzen P.Lee J.Polakow P.B.Andrews S.Issar D.Nesmith H.Gommerstadt L.Jia D.Griffith J.A.Pérez S.McLaughlin W.Lovas K.Crary R.Harper B.Pientka A.Momigliano M.Kohlhase J.Hannan S.Michaylov T.Freeman C.Elliott G.Price S.Park S.Thrun P.Wickline J.Despeyroux S.Balzer F.Cruz R.Rocha S.C.Goldstein H.DeYoung P.López K.Watkins T.M.VII L.Petersen G.Dowek T.Hardin C.Kirchner A.P.Felty E.L.Gunter D.Miller D.Nesmith C.P.Klapper

Talks about:

logic (25) type (20) linear (13) order (13) higher (11) session (10) program (8) system (7) unif (7) theorem (6)

Person: Frank Pfenning

DBLP: Pfenning:Frank

Facilitated 4 volumes:

Contributed to:

2015

2014

2013

2012

2011

2009

2008

2007

2006

2005

2004

2003

2001

2000

1999

1998

1997

1996

1995

1994

1993

1992

1991

1990

1989

1988

1986

1984

1989

2018

2019

2016

Wrote 70 papers:

FoSSaCS-2015-PfenningG: Polarized Substructural Session Types (FP, DG), pp. 3–22.
ICLP-J-2014-CruzRGP #concurrent #graph #linear #logic programming #programming language: A Linear Logic Programming Language for Concurrent Programming over Graph Structures (FC, RR, SCG, FP), pp. 493–507.
ESOP-2013-CairesPPT #behaviour #communication #morphism #parametricity #polymorphism: Behavioral Polymorphism and Parametricity in Session-Based Communication (LC, JAP, FP, BT), pp. 330–349.
ESOP-2013-ToninhoCP #higher-order #integration #monad #process: Higher-Order Processes, Functions, and Sessions: A Monadic Integration (BT, LC, FP), pp. 350–369.
CSL-2012-DeYoungCPT #communication #linear #logic #reduction: Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication (HD, LC, FP, BT), pp. 228–242.
ESOP-2012-PerezCPT #concurrent #linear #logic: Linear Logical Relations for Session-Based Concurrency (JAP, LC, FP, BT), pp. 539–558.
FoSSaCS-2012-ToninhoCP #process: Functions as Session-Typed Processes (BT, LC, FP), pp. 346–360.
PPDP-2011-ToninhoCP #linear #type system: Dependent session types via intuitionistic linear type theory (BT, LC, FP), pp. 161–172.
CADE-2009-McLaughlinP #performance #proving #theorem proving: Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method (SM, FP), pp. 230–244.
LICS-2009-PfenningS #logic programming #order #semantics: Substructural Operational Semantics as Ordered Logic Programming (FP, RJS), pp. 101–110.
PEPM-2009-SimmonsP #approximate #linear #logic: Linear logical approximations (RJS, FP), pp. 9–20.
TLCA-2009-LovasP #proving #refinement: Refinement Types as Proof Irrelevance (WL, FP), pp. 157–171.
ICALP-B-2008-SimmonsP #algorithm #linear #logic: Linear Logical Algorithms (RJS, FP), pp. 336–347.
ICFP-2007-Pfenning #revisited #type system: Subtyping and intersection types revisited (FP), p. 219.
RTA-2007-Pfenning #logic #on the: On a Logical Foundation for Explicit Substitutions (FP), p. 19.
TLCA-2007-Pfenning #logic #on the: On a Logical Foundation for Explicit Substitutions (FP), p. 1.
IJCAR-2006-ChaudhuriPP #logic: A Logical Characterization of Forward and Backward Chaining in the Inverse Method (KC, FP, GP), pp. 97–111.
CADE-2005-ChaudhuriP #first-order #linear #logic #proving #theorem proving: A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (KC, FP), pp. 69–83.
CSL-2005-ChaudhuriP #linear #logic: Focusing the Inverse Method for Linear Logic (KC, FP), pp. 200–215.
POPL-2005-ParkPT #probability: A probabilistic language based upon sampling functions (SP, FP, ST), pp. 171–182.
PPDP-2005-LopezPPW #concurrent #linear #logic programming #monad: Monadic concurrent linear logic programming (PL, FP, JP, KW), pp. 35–46.
LICS-2004-VIICHP #distributed #symmetry #λ-calculus: A Symmetric Modal λ Calculus for Distributed Computing (TMV, KC, RH, FP), pp. 286–295.
POPL-2004-DunfieldP #bidirectional: Tridirectional typechecking (JD, FP), pp. 281–292.
CADE-2003-PientkaP #higher-order #optimisation #unification: Optimizing Higher-Order Pattern Unification (BP, FP), pp. 473–487.
FoSSaCS-2003-DunfieldP #call-by: Type Assignment for Intersections and Unions in Call-by-Value Languages (JD, FP), pp. 250–266.
POPL-2003-PetersenHCP #layout #memory management #type system: A type theory for memory allocation and data layout (LP, RH, KC, FP), pp. 172–184.
LICS-2001-Pfenning #proving #type system: Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory (FP), pp. 221–230.
ICFP-2000-DaviesP: Intersection types and computational effects (RD, FP), pp. 198–208.
PEPM-2000-Pfenning #logic #on the #staged: On the Logical Foundations of Staged Computation (FP), p. 33.
SAIG-2000-Pfenning #reasoning #staged: Reasoning about Staged Computation (FP), pp. 5–6.
CADE-1999-PfenningS #deduction #framework #logic: System Description: Twelf — A Meta-Logical Framework for Deductive Systems (FP, CS), pp. 202–206.
ICLP-1999-MomiglianoP #higher-order #problem: The Relative Complement Problem for Higher-Order Patterns (AM, FP), pp. 380–394.
POPL-1999-XiP #dependent type #programming: Dependent Types in Practical Programming (HX, FP), pp. 214–227.
PPDP-1999-Pfenning #framework #logic: Logical and Meta-Logical Frameworks (FP), p. 206.
TLCA-1999-PolakowP #deduction #linear #logic: Natural Deduction for Intuitionistic Non-communicative Linear Logic (JP, FP), pp. 295–309.
CADE-1998-Pfenning #deduction #linear #logic #reasoning: Reasoning About Deductions in Linear Logic (FP), pp. 1–2.
CADE-1998-SchurmannP #automation #logic #proving #theorem proving: Automated Theorem Proving in a Simple Meta-Logic for LF (CS, FP), pp. 286–300.
PLDI-1998-WicklineLP #code generation #runtime: Run-time Code Generation and Modal-ML (PW, PL, FP), pp. 224–235.
PLDI-1998-XiP #array #bound #dependent type: Eliminating Array Bound Checking Through Dependent Types (HX, FP), pp. 249–257.
LICS-1997-CervesatoP #higher-order #linear: Linear Higher-Order Pre-Unification (IC, FP), pp. 422–433.
TLCA-1997-DespeyrouxPS #higher-order #recursion #syntax: Primitive Recursion for Higher-Order Abstract Syntax (JD, FP, CS), pp. 147–163.
ESOP-1996-RohwedderP #higher-order #logic programming #source code #termination: Mode and Termination Checking for Higher-Order Logic Programs (ER, FP), pp. 296–310.
JICSLP-1996-DowekHKP #higher-order #unification: Unification via Explicit Substitutions: The Case of Higher-Order Patterns (GD, TH, CK, FP), pp. 259–273.
LICS-1996-CervesatoP #framework #linear #logic: A Linear Logical Framework (IC, FP), pp. 264–275.
POPL-1996-DaviesP #analysis #staged: A Modal Analysis of Staged Computation (RD, FP), pp. 258–270.
LICS-1995-Pfenning: Structural Cut Elimination (FP), pp. 156–166.
CADE-1994-Pfenning #deduction #metalanguage #named: Elf: A Meta-Language for Deductive Systems (FP), pp. 811–815.
ILPS-1993-KohlhaseP #unification #λ-calculus: Unification in a λ-Calculus with Intersection Types (MK, FP), pp. 488–505.
CADE-1992-PfenningR #deduction #implementation: Implementing the Meta-Theory of Deductive Systems (FP, ER), pp. 537–551.
LICS-1992-PfenningH #compilation #verification: Compiler Verification in LF (JH, FP), pp. 407–418.
ISLP-1991-DietzenP #declarative #logic programming: A Declarative Alternative to “Assert” in Logic Programming (SD, FP), pp. 372–386.
LICS-1991-Pfenning #anti #calculus #unification: Unification and Anti-Unification in the Calculus of Constructions (FP), pp. 74–85.
PEPM-1991-MichaylovP #compilation #polymorphism #λ-calculus: Compiling the Polymorphic λ-Calculus (SM, FP), pp. 285–296.
PLDI-1991-FreemanP #ml #refinement: Refinement Types for ML (TF, FP), pp. 268–277.
CADE-1990-AndrewsINP #proving #theorem proving: The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 641–642.
CADE-1990-FeltyGMP #prolog #tutorial #λ-calculus: Tutorial on Lambda-Prolog (APF, ELG, DM, FP), p. 682.
CADE-1990-PfenningN #deduction #symmetry: Presenting Intuitive Deductions via Symmetric Simplification (FP, DN), pp. 336–350.
CLP-1990-Pfenning90 #logic programming: Types in Logic Programming (FP), p. 786.
LICS-1989-Pfenning #logic #metaprogramming #named: Elf: A Language for Logic Definition and Verified Metaprogramming (FP), pp. 313–322.
ML-1989-DietzenP #framework #higher-order #logic: Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization (SD, FP), pp. 447–449.
CADE-1988-AndrewsINP #proving #theorem proving: The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 760–761.
CADE-1988-Pfenning #axiom #calculus: Single Axioms in the Implicational Propositional Calculus (FP), pp. 710–713.
LFP-1988-Pfenning #higher-order #polymorphism #type inference #unification: Partial Polymorphic Type Inference and Higher-Order Unification (FP), pp. 153–163.
PLDI-1988-PfenningE #higher-order #syntax: Higher-Order Abstract Syntax (FP, CE), pp. 199–208.
CADE-1986-AndrewsPIK #proving #theorem proving: The TPS Theorem Proving System (PBA, FP, SI, CPK), pp. 663–664.
CADE-1984-Pfenning #proving: Analytic and Non-analytic Proofs (FP), pp. 394–413.
CCIPL-1989-PfenningL #morphism #named #polymorphism: LEAP: A Language with Eval And Polymorphism (FP, PL), pp. 345–359.
ESOP-2018-GommerstadtJP #concurrent #contract: Session-Typed Concurrent Contracts (HG, LJ, FP), pp. 771–798.
ESOP-2019-BalzerTP: Manifest Deadlock-Freedom for Shared Session Types (SB, BT, FP), pp. 611–639.
POPL-2016-JiaGP #higher-order #monitoring: Monitors and blame assignment for higher-order session types (LJ, HG, FP), pp. 582–594.