Research Interests Programming Languages, Logic and Type Theory, Logical Frameworks, Automated Deduction, Trustworthy Computing (see also Publications, Students & Co-authors) Projects Logosphere A Formal Digital Library Triple Type Refinement in Programming Languages ConCert Language Technology for Trustless Software Dissemination Twelf Logical and Meta-Logical Frameworks SeLF Distributed System Security via Logical Frameworks Manifest Security Logics and Languages for Manifestly Secure Systems Prospero Integrating Types and Specifications
Class 1: Overview * Arithmetic expressions * Arithmetic expressions with let-binding o Variation: Call-by-value let-binding syntax o Variation: Defining evaluation with a hypothetical judgement * Typed arithmetic expressions o Variation: Typed arithmetic expressions (extrinsic encoding) * Exercises 1 Class 2: Representation * Mechanizing Metatheory in a Logical Framework discusses this material in detail. * Exercises 2 Class 3: Mechanizing Metatheory * Type safety for MinML (intrinsic encoding) * Type safety for MinML (extrinsic encoding) * Exercises 3 Additional reading * PFPL: We will use Practical Foundations for Programming Languages as a reference for basic PL concepts. * MMLF: Mechanizing Metatheory in a Logical Framework discusses LF, representation, and mechanized metatheory in technical detail. * Proving metatheorems with Twelf is a self-contained intro tutorial