Pure and Applied Logic
The Pure and Applied Logic (PAL) program is an interdisciplinary Ph.D. program at
Carnegie Mellon University
with faculty from:
The program builds upon Carnegie Mellon's unique strengths in logic and its applications to computer science. Internationally recognized faculty, frequent workshops, colloquia, seminar series, and excellent computing facilities contribute to an ideal environment for both theoretical and applied research. Graduates of the program have gone on to prominent positions in industry and academe.
Carnegie Mellon ranks highly in logic and related fields; see the
university-maintained summary of rankings of
various departments and programs at Carnegie Mellon.
Areas of strength include:
- automated theorem proving
- category theory and categorical logic
- constructive mathematics
- foundations of decision theory
- foundations of programming languages
- logics of programs
- lambda calculus
- learning theory
- model theory
- proof theory
- set theory
- temporal and modal logics
- theory of computing
- type theory
Related research at Carnegie Mellon includes algorithms, artificial intelligence, combinatorial optimization, computational complexity, computational linguistics, operations research, and programming systems. See also the logic bibliography maintained at Carnegie Mellon.
Students interested in applying for admission to PAL should consult our
answers to frequently asked questions.
Program faculty
-
Peter Andrews
Professor of
Mathematics
mathematical logic, automated theorem proving, type theory
-
Horacio
Arlo Costa
Associate Professor of Philosophy
philosophical logic, epistemology, knowledge representation
-
Jeremy Avigad
Associate Professor of
Philosophy
mathematical logic, proof theory, automated theorem proving, history and philosophy of mathematics
-
Steve Awodey
Associate Professor of
Philosophy
category theory, logic, philosophy of mathematics, history of logic and analytic philosophy
-
Lenore Blum
Distinguished Career Professor of Computer Science
computational complexity, real computation
-
Stephen
Brookes
Professor of Computer Science
mathematical semantics of programming languages
-
Edmund Clarke
FORE Systems Professor of Computer Science and Professor of Electrical and Computer Engineering
automatic verification of computer hardware and software
-
James Cummings
Associate Professor of Mathematical Sciences
mathematical logic, set theory
- David Danks
Assistant Professor of
Philosophy
causal learning, cognitive science, philosophy of psychology, philosophy of science
-
Clark
Glymour
Alumni University Professor of Philosophy
philosophy of science, causal modeling, cognitive science, machine learning
-
Rami Grossberg
Associate Professor of
Mathematical Sciences
mathematical logic, model theory
-
Robert Harper
Professor of Computer Science
type theory, logical frameworks, programming languages
-
Kevin Kelly
Professor of
Philosophy
epistemology, philosophy of science, learning theory, computability,
Ockham's razor
-
Peter Lee
Professor of
Computer Science
foundations of programming languages, proof carrying code
-
Frank Pfenning
Professor of
Computer Science and Philosophy
programming languages, logic and type theory, logical frameworks, automated deduction, trustworthy computing
-
John Reynolds
Professor of
Computer Science
semantics of programming languages
-
Richard
Scheines
Professor of Philosophy, Machine Learning, and Human Computer Interaction
graphical and statistical causal inference, philosophy of social science, foundations of causation, educational technology
-
Ernest
Schimmerling
Associate Professor of
Mathematical Sciences
mathematical logic, set theory
-
Dana Scott
Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic (Emeritus)
mathematical logic, model theory, set theory, foundations of logic and mathematics, symbolic mathematical computation
-
Teddy
Seidenfeld
H.A. Simon Professor of Philosophy, Statistics, and Machine Learning
foundations of statistics, decision theory
-
Wilfried Sieg
Professor of
Philosophy
philosophy of mathematics, proof theory, automated proof search, history of
modern logic, computability theory
-
Mandy
Simons
Associate Professor of
Philosophy
philosophy of language, formal semantics and pragmatics of natural language
-
Peter
Spirtes
Professor of
Philosophy and Machine Learning
graphical and statistical causal inference, causation in the social sciences, philosophy of physics
-
Richard Statman
Professor of
Computer Science and Mathematical Sciences
mathematical logic, theory of computation, lambda calculus, combinatory logic
Current and upcoming logic events
Logic course offerings
The three PAL departments offer many beginning, intermediate
and advanced graduate logic courses.
Beginning courses are repeated every year with more or less the same
content each time whereas the topics covered in intermediate
and advanced courses vary. Courses that are offered on a regular or semiregular basis include:
- 15-812 Semantics of Programming Languages
- 15-814 Type Systems for Programming Languages
- 15-819 Hardware and Software Verification
- 21-600 Mathematical Logic I
- 21-602 Set Theory I
- 21-603 Model Theory I
- 21-700 Mathematical Logic II
- 21-702 Set Theory II
- 21-703 Model Theory II
- 21-800 Advanced Topics in Logic
- 21-804 Math Logic Seminar
- 21-805 Lambda Calculus
- 80-610 Logic and Computation
- 80-615 Modal Logic
- 80-611 Computability and Incompleteness
- 80-612 Philosophy of Mathematics
- 80-618 Computability and Proof Search
- 80-619 Computability and Learnibility
- 80-711 Proof Theory
- 80-713 Category Theory
- 80-813 Seminar on Philosophy of Mathematics
- 80-820 Categorical Logic
One can read off departments from course numbers according to:
- 15-xxx Computer Science
- 21-xxx Mathematical Sciences
- 80-xxx Philosophy
Before each semester, a list of
courses and descriptions for the upcoming term is published here.
Click here to send e-mail to the webmaster.