Pure and Applied Logic

• the Department of Computer Science in the School of Computer Science
• the Department of Mathematical Sciences in the Mellon College of Science
• the Department of Philosophy in the College of Humanities and Social Sciences

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
• formal verification
• 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
  Professor of Philosophy and Mathematical Sciences
  mathematical logic, proof theory, automated theorem proving, history and philosophy of mathematics
   
• Steve Awodey
  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
  Associate 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
   
• André Platzer
  Assistant Professor of Computer Science
  logics of hybrid systems, logics of programs, automated theorem proving, proof theory, automatic verification, and hybrid systems verification
   
• 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
  Patrick Suppes 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

• Mathematical Logic Seminar
• Philosophy Colloquium
• Appalachian Set Theory

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.

• PAL courses, Fall 2009
• PAL courses, Spring 2009
• PAL courses, Fall 2008
• PAL courses, Spring 2008
• PAL courses, Fall 2007
• PAL courses, Spring 2007
• PAL courses, Fall 2006
• PAL courses, Spring 2006
• PAL courses, Fall 2005
• PAL courses, Spring 2005
• PAL courses, Fall 2004

Click here to send e-mail to the webmaster.