Frank Pfenning

Last updated
Frank Pfenning
Frank Pfenning.jpg
Mathematical Foundations of Programming Semantics (Pittsburgh, May 2004)
Born
Education Technische Universität Darmstadt
Carnegie Mellon University
SpouseNancy Pfenning
Awards ACM Fellow (2015)
Scientific career
Institutions Carnegie Mellon University
Doctoral advisor Peter B. Andrews
Doctoral students
Website http://www.cs.cmu.edu/~fp/

Frank Pfenning is a German-American professor of computer science, adjunct professor in the department of philosophy, and head of the Computer Science Department at Carnegie Mellon University. [1]

Contents

Education and career

Pfenning grew up in Rüsselsheim in Germany. He studied mathematics and computer science at Technische Universität Darmstadt in Germany. He then moved to the US and studied at Carnegie Mellon University, where he received his M.S. and Ph.D. in the Department of Mathematics in 1987, for his dissertation entitled Proof Transformations in Higher-Order Logic. He was a student of Peter B. Andrews.

His research includes work in the area of programming languages, logic and type theory, logical frameworks, automated deduction, and trustworthy computing. He is one of the principal authors of the Twelf system. He also developed Carnegie Mellon's introductory imperative programming course for undergraduates and the C0 programming language used in this course.

Honors and awards

In 2015 he was named a Fellow of the Association for Computing Machinery "for contributions to the logical foundations of automatic theorem proving and types for programming languages." [2] In 2016 he received the LICS Test of Time Award for the paper "A Linear Logical Framework", [3] co-authored with Iliano Cervesato.

Personal life

Pfenning is a competitive squash player, ranked in the top five of the university's squash ladder. [4]

Pfenning has also appeared in an experimental film alongside Sharon Needles. [5] [6]

Related Research Articles

<span class="mw-page-title-main">Carnegie Mellon University</span> Private research university in Pittsburgh, Pennsylvania, U.S.

Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania. The institution was originally established in 1900 by Andrew Carnegie as the Carnegie Technical Schools. In 1912, it became the Carnegie Institute of Technology and began granting four-year degrees. In 1967, it became the current-day Carnegie Mellon University through its merger with the Mellon Institute of Industrial Research, founded in 1913 by Andrew Mellon and Richard B. Mellon and formerly a part of the University of Pittsburgh.

<span class="mw-page-title-main">Dana Scott</span> American logician (born 1932)

Dana Stewart Scott is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, California. His work on automata theory earned him the Turing Award in 1976, while his collaborative work with Christopher Strachey in the 1970s laid the foundations of modern approaches to the semantics of programming languages. He has also worked on modal logic, topology, and category theory.

<span class="mw-page-title-main">Carnegie Mellon School of Computer Science</span> School for computer science in the United States

The School of Computer Science (SCS) at Carnegie Mellon University in Pittsburgh, Pennsylvania, US is a school for computer science established in 1988. It has been consistently ranked among the top computer science programs over the decades. As of 2022 U.S. News & World Report ranks the graduate program as tied for second with Stanford University and University of California, Berkeley. It is ranked second in the United States on Computer Science Open Rankings, which combines scores from multiple independent rankings.

<span class="mw-page-title-main">Allen Newell</span> American cognitive scientist

Allen Newell was an American researcher in computer science and cognitive psychology at the RAND Corporation and at Carnegie Mellon University's School of Computer Science, Tepper School of Business, and Department of Psychology. He contributed to the Information Processing Language (1956) and two of the earliest AI programs, the Logic Theorist (1956) and the General Problem Solver (1957). He was awarded the ACM's A.M. Turing Award along with Herbert A. Simon in 1975 for their contributions to artificial intelligence and the psychology of human cognition.

<span class="mw-page-title-main">Alan Perlis</span> American computer scientist (1922–1990)

Alan Jay Perlis was an American computer scientist and professor at Purdue University, Carnegie Mellon University and Yale University. He is best known for his pioneering work in programming languages and was the first recipient of the Turing Award.

In logic, a logical framework provides a means to define a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving. The first logical framework was Automath; however, the name of the idea comes from the more widely known Edinburgh Logical Framework, LF. Several more recent proof tools like Isabelle are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human-machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory.

<span class="mw-page-title-main">John C. Reynolds</span> American computer scientist (1935–2013)

John Charles Reynolds was an American computer scientist.

The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.

<span class="mw-page-title-main">Human–Computer Interaction Institute</span>

The Human–Computer Interaction Institute (HCII) is a department within the School of Computer Science at Carnegie Mellon University (CMU) in Pittsburgh, Pennsylvania. It is considered one of the leading centers of human–computer interaction research, and was named one of the top ten most innovative schools in information technology by Computer World in 2008. For the past three decades, the institute has been the predominant publishing force at leading HCI venues, most notably ACM CHI, where it regularly contributes more than 10% of the papers. Research at the institute aims to understand and create technology that harmonizes with and improves human capabilities by integrating aspects of computer science, design, social science, and learning science.

<span class="mw-page-title-main">Manuela M. Veloso</span> Portuguese-American computer scientist

Manuela Maria Veloso is the Head of J.P. Morgan AI Research & Herbert A. Simon University Professor Emeritus in the School of Computer Science at Carnegie Mellon University, where she was previously Head of the Machine Learning Department. She served as president of Association for the Advancement of Artificial Intelligence (AAAI) until 2014, and the co-founder and a Past President of the RoboCup Federation. She is a fellow of AAAI, Institute of Electrical and Electronics Engineers (IEEE), American Association for the Advancement of Science (AAAS), and Association for Computing Machinery (ACM). She is an international expert in artificial intelligence and robotics.

<span class="mw-page-title-main">Gary Miller (computer scientist)</span> American computer scientist

Gary Lee Miller is a professor of Computer Science at Carnegie Mellon University, Pittsburgh, United States. In 2003 he won the ACM Paris Kanellakis Award for the Miller–Rabin primality test. He was made an ACM Fellow in 2002 and won the Knuth Prize in 2013.

Srinivasan "Srini" Seshan is an American computer scientist and a professor of computer science at Carnegie Mellon University, specializing in computer networks.

<span class="mw-page-title-main">Eric Xing</span>

Eric Poe Xing is an American computer scientist whose research spans machine learning, computational biology, and statistical methodology. Xing is founding President of the world’s first artificial intelligence university, Mohamed bin Zayed University of Artificial Intelligence (MBZUAI).

<span class="mw-page-title-main">Prakash Panangaden</span> American/Canadian computer scientist

Prakash Panangaden is an American/Canadian computer scientist noted for his research in programming language theory, concurrency theory, Markov processes and duality theory. Earlier he worked on quantum field theory in curved space-time and radiation from black holes. He is the founding Chair of the ACM Special Interest Group on Logic and Computation.

Maria-Florina (Nina) Balcan is a Romanian-American computer scientist whose research investigates machine learning, algorithmic game theory, theoretical computer science, including active learning, kernel methods, random-sampling mechanisms and envy-free pricing. She is an associate professor of computer science at Carnegie Mellon University.

<span class="mw-page-title-main">Gerald Penn (computer scientist)</span> American computer scientist

Gerald Penn is an American computer scientist specializing in mathematical linguistics and speech processing. He is a Professor of Computer Science at the University of Toronto, a senior member of IEEE and AAAI, and a past chair of Association for Mathematics of Language.

Dale Miller is an American computer scientist and author. He is a Director of Research at Inria Saclay and one of the designers of the λProlog programming language and the Abella interactive theorem prover.

<span class="mw-page-title-main">Kenneth L. McMillan</span> American computer scientist

Kenneth L. McMillan is an American computer scientist working in the area of formal methods, logic, and programming languages. He is a professor in the computer science department at the University of Texas at Austin, where he holds the Admiral B.R. Inman Centennial Chair in Computing Theory.

References

  1. "Frank Pfenning Named Head of Carnegie Mellon's Computer Science Department". January 8, 2013. Retrieved 9 January 2013.
  2. ACM Fellows Named for Computing Innovations that Are Advancing Technology in the Digital Age, Association for Computing Machinery, 2015, archived from the original on 2015-12-09, retrieved 2015-12-10.
  3. "LICS - Archive". lics.siglog.org. Retrieved 2019-09-27.
  4. "CMU Squash Ladder" . Retrieved 27 January 2019.
  5. "Frank Pfenning / Curriculum Vitae". www.cs.cmu.edu. Retrieved 2021-02-17.
  6. Sharon Needles, archived from the original on 2021-12-19, retrieved 2021-02-17