| |
Frank Pfenning
Courses
Current
-
15-819K Logic Programming
-
Fall 2006: TuTh 10:30-11:50, WeH 4623. 12 units.
Logic programming is a paradigm where computation arises from proof
search in a logic according to a fixed, predictable strategy. It
thereby unifies logical specification and implementation in a way that
is quite different from functional or imperative programming. This
course provides a thorough, modern introduction to logic programming.
It consists of a traditional lecture component and a project component.
The lecture component introduces the basic concepts and techniques of logic
programming followed by successive refinement towards more efficient
implementations or extensions to richer logical concepts. We plan
to cover a variety of logics and operational interpretations. The
project component will be one or several projects related to logic
programming.
Future
-
15-213 Introduction to Computer Systems
-
Spring 2007.
Past
-
15-213 Introduction to Computer Systems
-
Spring 2006: TuTh 9:00-10:20, WeH 7500. Mon recitations. 12 units.
This course provides a programmer's view of how computer systems
execute programs, store information, and communicate. It enables
students to become more effective programmers, especially in dealing
with issues of performance, portability and robustness. It also serves
as a foundation for courses on compilers, networks, operating systems,
and computer architecture, where a deeper understanding of systems-level
issues is required. Topics covered include: machine-level code and its
generation by optimizing compilers, performance evaluation and
optimization, computer arithmetic, memory organization and management,
networking technology and protocols, and supporting concurrent
computation.
-
15-815 Automated Theorem Proving
-
This course provides a thorough, hands-on introduction to automated
theorem proving. It consists of a traditional lecture component and a
joint project in which we will construct a theorem prover. The lecture
component introduces the basic concepts and techniques of logic followed
by successive refinement towards more efficient implementations. The
basic theorem proving paradigms we plan to cover are tableaux and the
inverse method, both of which are applicable to classical and
non-classical logics. In addition we will cover equational
reasoning and cooperating decision procedures.
Prerequisites: For undergraduates an undergraduate
logic course or 15-312. No prerequisites for graduate students.
-
15-312 Foundations of Programming Languages
-
This course discusses in depth many of the concepts underlying the
design, definition, implementation and use of modern programming
languages. Formal approaches to defining the syntax and semantics are
used to describe the fundamental concepts underlying programming
languages. A variety of programming paradigms are covered such as
imperative, functional, logic, and concurrent programming. In addition
to the formal studies, experience with programming in the languages is
used to illustrate how different design goals can lead to radically
different languages and models of computation.
Prerequisites: 15-212 Principles of Programming.
-
15-462 Computer Graphics
-
This course provides a basic introduction to Computer Graphics. Some
undergraduate follow-up courses such as and Computer Animation are
offered on a regular basis.
Prerequisites: 15-213 Introduction to Computer
Systems, 21-241 Matrix Algebra, 21-259 Calculus in Three Dimensions, or
equivalents.
-
15-816 Linear Logic
-
This graduate course provides an introduction to linear logic with an
emphasis on its applications in computer science. This includes the
theory of functional, logic and imperative programming languages. We
will also develop a linear type theory which will serve as a
meta-language in which the theory of programming languages with state
can be formalized effectively. An implementation of the type theory may
be available for practical experiments later in the semester.
Prerequisite:
General familiarity with functional programming and logic.
-
15-851 Computation and Deduction
-
This introductory graduate course explores the theory of programming
languages using deductive systems. Throughout the course we use the Twelf system to specify languages,
implement algorithms, and prove meta-theorems. A textbook to be published
by Cambridge University Press is in preparation.
-
15-399 Constructive Logic
-
A junior-level introduction to constructive logic and its applications in computer science.
Cross-listed as 80-317/617 in the Department of Philosophy.
-
15-453 Formal Languages, Automata and Computation
-
A senior-level introduction to formal languages, automata, computability,
and complexity.
-
15-212 Fundamental Structures of Computer Science II
-
A sophomore-level introduction to advanced programming techniques
using Standard ML.
-
15-816 Linear Logic
-
An introduction to linear logic with an emphasis on its applications
in computer science.
-
15-810 Advanced Topics Theory:
Logic Programming
-
A graduate level introduction to the theory and practice of logic
programming.
-
15-810 Advanced Topics Theory: Proofs and Programs
-
A graduate level introduction to constructive logic, proofs, and programs.
- Spring 1993, co-taught with Wilfried Sieg and Stanley Wainer,
Department of Philosophy
- Spring 1988
-
21-127 Introduction to Modern Mathematics
-
Undergraduate (freshman level) introduction to discrete mathematics using the Mathematica
symbolic computation system.
- Fall 1995, teaching assistant to Michael Albert, Department of Mathematics.
-
15-810 Advanced Topics Theory: Typed Lambda-Calculus
-
Graduate introduction to typed lambda-calculi and their relation to
programming languages.
- Spring 1990, co-taught with Robert Harper
-
15-810 Advanced Topics Theory: Programming Languages and Type Theory
-
Graduate introduction to functional programming and type theory.
-
15-810 Advanced Topics Theory: Inferential Programming
-
Graduate seminar on formal program development and program transformation.
- Fall 1986, co-taught with Eugene Rollins
-
Theory of Computation
-
Undergraduate (senior level) course on automata, formal languages, and computation.
- Spring 1982, co-taught with Dale Miller.
[ Home
| Contact
| Research
| Publications
| CV
| Students
]
[ Projects
| Courses
| Conferences
| Organizations
| Journals
]
[ Logical Frameworks
| Pittsburgh Squash Racquets Assocation
]
Frank Pfenning
|