Computation and Deduction - Carnegie Mellon School of Computer ...

practice in modern computer science and students of the theory of programming languages ...... The judgments are now mutually dependent to a large degree. ..... The instantiation of the type family vs is valid, since ev z : eval z z and val z :.
1MB Sizes 2 Downloads 322 Views
Computation and Deduction

Frank Pfenning Carnegie Mellon University

Draft of April 2, 1997 Draft notes for a course given at Carnegie Mellon University during the fall semester of 1994. Please send comments to [email protected] Do not cite, copy, or distribute without the express written consent of Frank Pfenning and the National Football League.

c Frank Pfenning 1992–1997 Copyright

ii

Contents 1 Introduction 1.1 The Theory of Programming Languages . . . . . . . . . . . . . . . . 1.2 Deductive Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3 Goals and Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 The 2.1 2.2 2.3 2.4 2.5 2.6 2.7 2.8

Mini-ML Language Abstract Syntax . . . . . . . . . . . . . . . . Substitution . . . . . . . . . . . . . . . . . . . Operational Semantics . . . . . . . . . . . . . A First Meta-Theorem: Evaluation Returns a The Type System . . . . . . . . . . . . . . . . Type Preservation . . . . . . . . . . . . . . . Further Discussion . . . . . . . . . . . . . . . Exercises . . . . . . . . . . . . . . . . . . . .

3 Formalization in a Logical Framework 3.1 The Simply-Typed Fragment of LF . . . . . 3.2 Higher-Order Abstract Syntax . . . . . . . 3.3 Representing Mini-ML Expressions . . . . . 3.4 Judgments as Types . . . . . . . . . . . . . 3.5 Adding Dependent Types to the Framework 3.6 Representing Evaluations . . . . . . . . . . 3.7 Meta-Theory via Higher-Level Judgments . 3.8 The Full LF Type Theory . . . . . . . . . . 3.9 Canonical Forms in LF . . . . . . . . . . . . 3.10 Summary and Further Discussion . . . . . . 3.11 Exercises . . . . . . . . . . . . . . . . . . . iii

. . . . . . . . . . .

. . . . . . . . . . . . Value . . . . . . . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

1 2 3 6

. . . . . . . .

9 9 12 13 17 20 24 28 31

. . . . . . . . . . .

37 38 40 45 50 53 56 63 71 74 76 79

iv 4 The 4.1 4.2 4.3 4.4 4.5 4.6

CONTENTS Elf Programming Language Concrete Syntax . . . . . . . . . . . . . Type and Term Reconstruction . . . . . A Mini-ML Interpreter in Elf . . . . . . An Implementation of Value Soundness Dynamic and Static Constants . . . . . Exercises . . . . . . . . . . . . . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

81 . 83 . 84 . 88 . 97 . 101 . 105

5 Parametric and Hypothetical Judgments 5.1 Closed Expressions . . . . . . . . . . . . . . . 5.2 Function Types as Goals in Elf . . . . . . . . 5.3 Negation . . . . . . . . . . . . . . . . . . . . . 5.4 Representing Mini-ML Typing Derivations . . 5.5 An Elf Program for Mini-ML Type Inference 5.6 Representing the Proof of Type Preservation 5.7 Exercises . . . . . . . . . . . . . . . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .