Frank Pfenning | |
---|---|
Born | Rüsselsheim am Main, Germany |
Education | Technische Universität Darmstadt Carnegie Mellon University |
Spouse | Nancy 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]
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.
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.
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]
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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).
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.
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.
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.