Jan Hoffmann –

Transcript

1 Jan Hoffmann Carnegie Mellon University – Computer Science Department +1 412 268 6309 • [email protected] • Œ www.cs.cmu.edu/~janh Ó Q Research Interests My mission is to discover beautiful mathematical ideas that have a real-world impact, shape the way programmers think, and help to create better software. I am currently working on quantitative verification, type systems, static resource analysis of programs, probabilistic programming, proof assistants, and programming languages for digital contracts. Education Ludwig-Maximilians-Universität and TU Munich Munich 2008–2011 Ph.D. in Computer Science Advisor: Prof. Martin Hofmann. Grade: magna cum laude. Topic: Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. Munich Ludwig-Maximilians-Universität 2001–2007 Diplom mit Auszeichnung (Master with Honors in Computer Science) Grade: 1.0 (best possible). Major: Theoretical Computer Science. Minor subject: Mathematics. Positions Carnegie Mellon University Pittsburgh Tenure-Track Assistant Professor 2015–present In the Computer Science Department of the School of Computer Science. Yale University New Haven Associate Research Scientist 2012–2015 Topic: Quantitative Verification. Support: NSF VeriQ (PI) and DARPA HACMS (Key Personnel). Yale University New Haven 2011–2012 Postdoctoral Associate In the group of Prof. Zhong Shao. Topic: Verification of Lock-Free Data Structures. Support: DARPA HACMS (Key Personnel) and DARPA CRASH. Microsoft Research Cambridge, UK Feb. – Apr. 2011 Research Intern Mentors: Andrew Kennedy and Nick Benton. Topic: Operational Semantics in Coq. Ludwig-Maximilians-Universität and TU Munich Munich Research Assistant 2007–2011 In the group of Prof. Martin Hofmann. Topic: Automatic Resource Bound Analysis. University of California, San Diego San Diego Master Thesis Jan. – Jun. 2007 Advisor: Prof. Samuel R. Buss. Topic: DLL Algorithms and Resolution Proofs. Professional Activities Organizer Martin Hofmann Memorial Meeting , with L. Beringer, S. Jost, U. Schöpp, and D. Sannella 2019 19th Workshop on Logic and Computational Complexity (LCC’18) (Co-Chair) 2018 3rd Logic Mentoring Workshop (LMW’18) (Co-Chair) 2018 1/9

2 Dagstuhl Seminar Resource Bound Analysis 2017 , with M. Gaboardi, R. Wilhelm, and F. Zuleger (Co-Chair) 2016 LOLA 2016 - Syntax and Semantics of Low-Level Languages Annual PUMA Workshop, Venice, Italy. 2009 Guest Editor Automatic Resource Bound Analysis 2015–17 Journal of Automated Reasoning, Special Issue Committee Member Program Committee – LOLA 2019 - Syntax and Semantics of Low-Level Languages 2019 Program Committee – European Symposium on Programming (ESOP’20) 2019 2018–pres. Steering Committee – Logic Mentoring Workshop Program Committee – Symposium on Principles of Programming Languages (POPL’19) 2018 Review Panel – National Science Foundation (NSF) 2018 2018 Program Committee – Student Research Competition at PLDI 2018 (PLDI’18 SRC) Program Committee – International Colloquium on Automata, Languages and Programming (ICALP’18) 2018 2017 Program Committee – European Symposium on Programming (ESOP’18) Program Committee – Joint Workshop on Developments in Implicit Computational Complexity and Foundational and Practical Aspects of Resource Analysis (DICE-FOPARA’17) 2017 Program Committee – Int. Conf. on Formal Structures for Computation and Deduction (FSCD’17) 2017 Program Committee – Conf. on Programming Language Design and Implementation (PLDI’17) 2016–17 2016 External Review Committee – Conference on Computer Aided Verification (CAV’16) 2015 Program Committee – Conf. on Found. of Software Science and Comp. Structures (FOSSACS’16) Program Committee – Developments in Implicit Computational Complexity (DICE’15) 2015 External Review Committee – Symposium on Principles of Programming Languages (POPL’15) 2014 University Service Ph.D. Admissions Committee – Computer Science Department, Carnegie Mellon 2019–2020 Organizer of the Computer Science Department’s Open House – Carnegie Mellon 2019–2020 Member of the Doctoral Review Committee – Computer Science Department, Carnegie Mellon 2018–pres. 2015–pres. Organizer of the weekly PLunch Meeting – Carnegie Mellon 2015–pres. Organizer of the PoP Seminar – Carnegie Mellon Master Admission Committee – Computer Science Department, Carnegie Mellon 2015-2016 Teaching and Mentoring Current PhD Students and Post-Docs Stefan Muller, Post-Doc 2018–present David Kahn, PhD Student 2018–present Di Wang, PhD Student 2017–present Ankush Das, PhD Student 2015–present Current BS Students Charles Yuan, BS Student 2018–present Former Students Prachi Laud, BS Student (now Software Engineer at Facebook) 2017–2018 Yue Niu, BS Student (now PhD students at Carnegie Mellon) 2017–2018 2016–2018 Chan Ngo, Post-Doc (now Senior Research Engineer at Aptiv) Nicholas Roberts, BS Student 2018–2019 2016–2017 Benjamin Lichtman, BS Student (now Software Engineer at Microsoft) Quentin Carbonneaux, PhD Student (co-advised with Zhong Shao) 2013–2017 Courses Taught 15-312: Principles of Programming Languages (with Stephanie Balzer) Carnegie Mellon, Spring 2019 15-411/15-611: Compiler Design Carnegie Mellon, Fall 2018 Introduction to Types and Semantics Oregon PL Summer School, Summer 2018 15-312: Principles of Programming Languages Carnegie Mellon, Spring 2018 15-411/15-611: Compiler Design Carnegie Mellon, Fall 2017 2/9

3 15-312: Principles of Programming Languages (with Bob Harper) Carnegie Mellon, Spring 2017 Carnegie Mellon, Fall 2016 15-411/15-611: Compiler Design Type-Based Resource Analysis Oregon PL Summer School, Summer 2016 Carnegie Mellon, Spring 2016 15-819: Advanced Topics in Programming Languages: Resource Analysis CPSC730: Advanced Formal Methods Topics (with Zhong Shao) Yale, Fall 2012 CPSP721: Advanced Programming Language Topics (with Zhong Shao) Yale, Spring 2012 Grants and Awards Gift 2019 Jane Street Capital Research Grant National Science Foundation (NSF) 2018–2021 SHF: Small: Resource-Guided Program Synthesis. PIs: Jan Hoffmann (CMU) and Nadia Polikarpova (UCSD). Title: $250,000 (CMU component). Award No. 1812876. Research Grant 2018–2022 National Science Foundation (NSF) SaTC: CORE: Medium: Automated Support for Writing High-Assurance Smart Contracts. PIs: Jan Hoffmann Title: (CMU), Bryan Parno (CMU), and Andrew Miller (UIUC). $800,000 (CMU component). Award No. 1801369. Research Contract 2018–2022 DARPA Assured Autonomy HRL subcontract. CMU PIs: J. Dolan, D. Held, J. Hoffmann, S. Mitch, F. Pfenning, and A. Platzer. Gift Jane Street Capital 2018 With Jean Yang Schmidt Sciences Grant The Eric and Wendy Schmidt Fund for Strategic Innovation 2017–2018 Title: An Automated Algorithm Designer. With Carl Kingsford, Nina Balcan, Mor Harchol-Balter, Guy Blelloch, Anupam Gupta, and Jan Hoffmann. Google Research Award 2016 Google Inc. Automated Static Resource Regression Analysis. Title: Dagstuhl Seminar (Organizer) Schloss Dagstuhl 2016 Resource Bound Analysis Title: . Date: July, 2017. With Marco Gaboardi, Reinhard Wilhelm, and Florian Zuleger. Research Contract DARPA STAC – Space/Time Analysis for Cybersecurity 2015–2019 Title: CURB: Calculating and Understanding Resource Bounds to Detect Space/Time Vulnerabilities. $6,230,090, 4 years, Award FA8750-15-C-0082 PIs: A. Loginov (GrammaTech), T. Reps (U Wisconsin), J. Hoffmann (CMU) and Z. Shao (Yale); Yale/CMU component: $1,448,531. Research Grant 2013–2016 National Science Foundation (NSF) Title: VeriQ: Formal Quantitative Software Verification in Realistic Application Scenarios. $449,721, 3 years, Award CCF-1319671, PIs: Zhong Shao and Jan Hoffmann. Ph.D. Scholarship DFG Research Training Group (Graduiertenkolleg) PUMA 2008–2011 PUMA is a joint graduate school (doctoral training center) of LMU Munich and TU Munich. It is supported by the German Research Foundation (DFG). Foreign Education Scholarship German National Academic Foundation (Studienstiftung) 2007 For a six months’ stay at University of California, San Diego. Student Scholarship German National Academic Foundation (Studienstiftung) 2005–2007 3/9

4 For studying computer science at Ludwig-Maximilians-Universität Munich. Software Quantitative CompCert A formally-verified C compiler that preserves quantitative properties 2013–present We modified Xavier Leroy’s CompCert compiler and used the Coq Proof Assistant to prove the preservation of quantitative properties during compilation of C to x86 assembly. This enables the verification of stack-space bounds at the C level. This artifact was approved by the (Project Website) PLDI’13 Artifact Evaluation Committee. 4 C B A compositional certified resource-bound analyzer for C programs 2013–present We designed and implemented a system for statically determining a symbolic bound on the resource usage of C programs. The system is based on a fully-automatic amortized resource analysis. (Project Website) Resource Aware ML A system for automatic derivation of resource bounds for functional programs 2009–present For my Ph.D., I designed and implemented a system that automatically derives polynomial resource bounds for functional programs at compile time. We are currently integrating the analysis systems with INRIA’s OCaml compiler. (Project Website) CertiKOS A formally-verified hypervisor kernel 2012–2015 In the DARPA HACMS and DARPA CRASH programs, we use the Coq Proof Assistant and the verified CompCert C compiler to implement and verify the realistic hypervisor kernel CertiKOS. (Project Website) Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . In Peer-Reviewed Conferences 1. D. Wang and J. Hoffmann. Type-guided worst-case input generation . In 46th Symposium on Principles of Programming Languages (POPL’19) , 2019. 2. Y. Niu and J. Hoffmann. Automatic space bound analysis for functional programs with garbage collection . In 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning , 2018. (LPAR’18) 3. A. Das, J. Hoffmann, and F. Pfenning. Parallel complexity analysis with temporal session types . 23rd International Conference on Functional Programming (ICFP’18) , 2018. In 4. A. Das, J. Hoffmann, and F. Pfenning. Work analysis with resource-aware session types . In 33th ACM/IEEE Symposium on Logic in Computer Science (LICS’18) , 2018. 5. V. C. Ngo, Q. Carbonneaux, and J. Hoffmann. Bounded expectations: Resource analysis for probabilistic programs . In , 2018. 39th Conference on Programming Language Design and Implementation (PLDI’18) 6. D. Wang, J. Hoffmann, and T. Reps. Pmaf: An algebraic framework for static analysis of probabilistic programs . In 39th Conference on Programming Language Design and Implementation (PLDI’18) , 2018. 7. B. Lichtman and J. Hoffmann. Arrays and References in Resource Aware ML . In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD’17) , 2017. PDF . 4/9

5 8. Q. Carbonneaux, J. Hoffmann, T. Reps, and Z. Shao. Automated Resource Analysis with Coq Proof Objects . 29th International Conference on Computer-Aided Verification (CAV’17) , 2017. . In PDF 9. V. C. Ngo, M. Dehesa-Azuara, M. Fredrikson, and J. Hoffmann. . Verifying and Synthesizing Constant-Resource Implementations with Types 38th IEEE Symposium on Security and Privacy (S&P ’17) , 2017. PDF . In 10. A. Das and J. Hoffmann. ML for ML: Learning Cost Semantics by Experiment . In 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17) , 2017. PDF . 11. E. Çiçek, G. Barthe, M. Gaboardi, D. Garg, and J. Hoffmann. Relational Cost Analysis . In , 2017. PDF . 44th Symposium on Principles of Programming Languages (POPL’17) 12. J. Hoffmann, A. Das, and S.-C. Weng. . Towards Automatic Resource Bound Analysis for OCaml 44th Symposium on Principles of Programming Languages (POPL’17) , 2017. Artifact submitted and In approved. PDF . 13. Q. Carbonneaux, J. Hoffmann, and Z. Shao. . Compositional Certified Resource Bounds 36th Conference on Programming Language Design and Implementation (PLDI’15) , 2015. Artifact In submitted and approved. PDF . 14. J. Hoffmann and Z. Shao. Automatic Static Cost Analysis for Parallel Programs . In 24th European Symposium on Programming (ESOP’15) , 2015. PDF . 15. J. Hoffmann and Z. Shao. Type-Based Amortized Resource Analysis with Integers and Arrays . 12th International Symposium on Functional and Logic Programming (FLOPS’14) PDF . In , 2014. 16. Q. Carbonneaux, J. Hoffmann, T. Ramananandro, and Z. Shao. End-to-End Verification of Stack-Space Bounds for C Programs . 35th Conference on Programming Language Design and Implementation (PLDI’14) In , 2014. Artifact submitted and approved. PDF . 17. G. Scherer and J. Hoffmann. Tracking Data-Flow with Open Closure Types . In 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’13) , 2013. PDF . 18. H. Liang, J. Hoffmann, X. Feng, and Z. Shao. Characterizing Progress Properties of Concurrent Objects via Contextual Refinements . 24th International Conference on Concurrency Theory (CONCUR’13) , 2013. In . PDF 19. J. Hoffmann, M. Marmar, and Z. Shao. Quantitative Reasoning for Proving Lock-Freedom . In 28th ACM/IEEE Symposium on Logic in Computer Science (LICS’13) , 2013. PDF . 20. J. Hoffmann, K. Aehlig, and M. Hofmann. Resource Aware ML . In 24rd International Conference on Computer Aided Verification (CAV’12) , 2012. PDF . 5/9

6 21. N. R. Krishnaswami, N. Benton, and J. Hoffmann. Higher-Order Functional Reactive Programming in Bounded Space . 39th Symposium on Principles of Programming Languages (POPL’12) , 2012. . In PDF 22. J. Hoffmann, K. Aehlig, and M. Hofmann. . Multivariate Amortized Resource Analysis 38th Symposium on Principles of Programming Languages (POPL’11) , 2011. PDF . In 23. J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Se- . mantics 8th Asian Symposium on Programming Languages (APLAS’10) , 2010. PDF . In 24. J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polynomial Potential . In , 2010. PDF . 19th European Symposium on Programming (ESOP’10) 25. D. Baumeister, F. Brandt, F. A. Fischer, J. Hoffmann, and J. Rothe. . The Complexity of Computing Minimal Unidirectional Covering Sets Algorithms and Complexity, 7th International Conference (CIAC’10) , 2010. PDF . In 26. F. Brandt, M. Brill, F. A. Fischer, and J. Hoffmann. The Computational Complexity of Weak Saddles . In , 2009. PDF . Algorithmic Game Theory, Second International Symposium (SAGT’09) In Peer-Reviewed Journals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27. J. Hoffmann and Z. Shao. Type-Based Amortized Resource Analysis with Integers and Arrays . J. Funct. Program. , 2015. PDF . 28. D. Baumeister, F. Brandt, F. A. Fischer, J. Hoffmann, and J. Rothe. The Complexity of Computing Minimal Unidirectional Covering Sets . , 2013. . Theory of Computing Systems PDF 29. J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis . , 2012. PDF . ACM Trans. Program. Lang. Syst. 30. F. Brandt, M. Brill, F. A. Fischer, and J. Hoffmann. The Computational Complexity of Weak Saddles . Theory of Computing Systems , 2010. PDF . 31. F. Brandt, M. Brill, F. Fischer, P. Harrenstein, and J. Hoffmann. Computing Shapley’s Saddles . ACM SIGecom Exchanges , 8, 2009. PDF . 32. J. Hoffmann. Finding a Tree Structure in a Resolution Proof is NP-Complete . , 410(21-23), 2009. PDF Theoretical Computer Science . 33. S. R. Buss, J. Hoffmann, and J. Johannsen. Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning . Logical Methods in Computer Science , 4(4), 2008. PDF . 34. S. R. Buss and J. Hoffmann. The NP-hardness of Finding a Directed Acyclic Graph for Regular Resolution . Theoretical Computer Science , 396(1-3), 2008. PDF . 6/9

7 Theses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35. J. Hoffmann. Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis . PhD . thesis, Ludwig-Maximilians-Universiät München, 2011. PDF 36. J. Hoffmann. . Diploma Thesis, LMU München, Resolution Proofs and DLL-Algorithms with Clause Learning . 2007. PDF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Other Papers 37. A. Das, S. Balzer, J. Hoffmann, and F. Pfenning. Resource-aware session types for digital contracts , 2019. Working paper. 38. T. Knoth, D. Wang, J. Hoffmann, and N. Polikarpova. Resource-guided program synthesis , 2019. Working paper. 39. D. Wang, J. Hoffmann, and T. Reps. , 2018. Working paper. A denotational semantics for nondeterminism in probabilistic programs Talks Resource-Aware Session Types Invited talk 4th Workshop on Behavioral Types (BEAT ’19); Lisbon, Portugal January 2019 Programming Languages for Smart Contracts October 2018 CyLab Partners Conference; Pittsburgh, PA Resource Analysis for Probabilistic Programs Invited talk at the meeting of the IFIP working group 1.9/2.15 “Verified Software”; Oxford, UK July 2018 Resource Analysis for Probabilistic Programs Invited talk at the 9th International Workshop on Developments in Implicit Computational Complexity (DICE ’18); Thessaloniki, Greece April 2018 Resource Analysis for Probabilistic Programs ESOP 2018 Program Committee Workshop; Paris, France December 2017 Resource Bound Analysis and Static Analysis Invited talk at the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE ’17); Heidelberg, Germany July 2017 Towards Automatic Resource Bound Analysis for OCaml January 2017 Symposium on Principles of Programming Languages (POPL’17); Paris, France Resource Aware ML University at Buffalo; Buffalo, NY December 2017 Invited talk at the 5th South of England Regional Programming Language Seminar; Oxford; UK January 2017 Max Planck Institute for Software Systems; Saarbrücken; Germany June 2016 Automatic Resource Bound Analysis and Linear Optimization at the workshop Beyond Worst-Case Analysis at the Simons Institute; Berkeley; CA November 2016 Invited talk Static Analysis for Finding Space/Time Vulnerabilities CyLab Partners Conference; Pittsburgh; PA September 2016 Type-Based Resource Analysis Lecture series at the Oregon Programming Languages Summer School); Eugene; OR June 2016 Certified Resource Bounds in the CompCert Compiler Invited talk at Mathematical Foundations of Programming Semantics (MFPS’16); Pittsburgh; PA Mai 2016 7/9

8 Resource Aware Programming Principles of Programming (PoP) Group Retreat; Seven Springs; PA October 2015 Compositional Certified Resource Bounds Conf. on Programming Language Design and Implementation (PLDI’15); Portland; OR June 2015 Automatic Static Cost Analysis for Parallel Programs April 2015 European Symposium on Programming (ESOP’15); London; UK Formal Reasoning about Quantitative Properties of Software University of Colorado Boulder; Boulder, CO March 2015 Carnegie Mellon University; Pittsburgh, PA February 2015 University of Illinois at Urbana-Champaign; Urbana-Champaign, IL February 2015 University of Waterloo; Waterloo ON, Canada January 2015 Heriot-Watt University; Edinburgh, UK January 2015 November 2014 TU Munich (Department of Computer Science); Munich, Germany October 2014 Boston University; Boston MA October 2014 Northeastern University; Boston MA April 2014 MIT; Boston MA Harvard University; Boston MA April 2014 Formal Verification of Quantitative Software Properties November 2014 TU Munich (Institute for Advanced Study); Munich, Germany End-to-End Verification of Stack-Space Bounds for C Programs Workshop on Higher Order Computation: Types, Complexity, Applications; Paris, France June 2014 Type-Based Amortized Resource Analysis with Integers and Arrays Int. Symp. on Functional and Logic Programming (FLOPS’14); Kanasawa, Japan June 2014 Tracking Data-Flow with Open Closure Types Int. Conf. on Logic for Prog., Art. Intel. and Reasoning (LPAR’13); Stellenbosch, South Africa December 2013 Characterizing Progress Properties of Concurrent Objects via Contextual Refinements DARPA HACMS-CARS site visit; New Haven, CT September 2013 Quantitative Reasoning for Proving Lock-Freedom ACM/IEEE Symposium on Logic in Computer Science (LICS’13); New Orleans, LA June 2013 University of Pennsylvania; Philadelphia, PA February 2013 DARPA CRASH PI meeting; San Diego, CA November 2012 DARPA CRASH-CertiKOS site visit; New Haven, CT October 2012 Resource Aware ML Int. Conf. on Computer Aided Verification (CAV’12); Berkeley, CA July 2012 Polynomial Amortized Resource Analysis DFG PUMA site visit; Munich, Germany June 2012 Dissertation defense at LMU; Munich, Germany October 2011 Higher-Order Functional Reactive Programming in Bounded Space October 2011 PUMA Workshop; Traunkirchen, Austria Multivariate Amortized Resource Analysis Université Paris 7 - Denis Diderot; Paris, France September 2011 UPENN; Philadelphia, PA June 2011 Yale University; New Haven, CT June 2011 IST Austria; Vienna, Austria June 2011 Microsoft Research; Cambridge, UK March 2011 Symposium on Principles of Programming Languages (POPL’11); Austin, TX January 2011 PUMA Workshop; Szentendre, Hungary October 2010 8/9

9 Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Op. Sem. Asian Symposium on Programming Languages (APLAS’10); Shanghai, China November 2010 Analysing Sorting Algorithms in Resource Aware ML November 2010 University of Kassel; Kassel, Germany Automatic Amortized Resource Analysis National DFG GK Workshop; Dagstuhl, Germany June 2010 Amortized Resource Analysis with Polynomial Potential European Symposium on Programming (ESOP’10); Cyprus March 2010 October 2009 PUMA Workshop; Venice, Italy A Purely-Functional SAT Solver PUMA Kickoff Meeting; Spitzingsee, Germany October 2008 DLL-Algorithms and Resolution Proofs September 2008 Fall School: Logic and Complexity; Prague, Czech Republic Languages German : Native English : Fluent French : Elementary References Prof. Zhong Shao, PhD Prof. Martin Hofmann, PhD Yale University LMU München Department of Computer Science Institut für Informatik 51 Prospect St. Oettingenstr. 67 New Haven, CT 06511, USA 80538 München, Germany Email: [email protected] Email: [email protected] Phone: +1 (203) 432 6828 Phone: +49 (89) 2180 9341 Nick Benton, PhD Prof. Andrew W. Appel, PhD Microsoft Research Princeton University 21 Station Road Department of Computer Science Cambridge CB1 2FB, UK 35 Olden St. Princeton, NJ 08540, USA Email: [email protected] Phone: +44 (1223) 479700 (reception) Email: [email protected] Phone: +1 (609) 258 4627 Prof. Frank Pfenning, PhD Carnegie Mellon University Computer Science Department 5000 Forbes Avenue Pittsburgh, PA 15213-3891, USA Email: [email protected] Phone: +1 (412) 268-6343 9/9

Related documents