Series: Penn State Logic Seminar

Date: Tuesday, February 12, 2002

Time: 2:30 - 3:45 PM

Place: 113 McAllister Building

Speaker: Pavel Naumov, Computer Science, Penn State Harrisburg

Title: Propositional Logic of Subtyping


We will introduce a new logical calculus that expresses subtyping
properties of Cartesian product and disjoint union type constructors.
The logic is formulated in standard propositional language and treats
conjunction as a product, disjunction as a disjoint union, and
implication as a type operation that generalizes subtyping relation.
The main result is a completeness theorem for this logic with respect
to a term semantics.