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 Abstract: 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.