Advancing the Type-Theoretic
Underpinnings of Practical Programming Languages
Karl Crary
Cornell University

KML Project

• Better programming language
• Rigorous semantics
• Efficient implementation
• Underlying philosophy
  View programming languages as a tractable approximation to foundational type theory

Better than What?

• C++
  

  

• Java
  OOP support
  More type safe
  Automatic memory management
  
• Modula=3
  More expressive modules
  Each retains most of the old shortcomings
  
• ML
  

  

• Want more:
  more expressive modules
  more expressive type system
  more efficient implementation
  
• Nuprl
  

  

KML Agenda

• Augment ML with:
  OOP support
  More expressive modules
  Richer type system
  Subtyping
  Higher order type constructors
• Better semantics
• Efficient implementation

Semantic Frameworks

• Reduction (``Subject-Reduction and Progress'')
  Shallow, almost syntactic, understanding
  Mainly for proving soundness of typing
• Structured operational semantics
• Denotational semantics

Type-Theoretic Semantics

• Define the meaning of KML in Nuprl's type theory
• Many semantic models
  Partial Equivalence Relations (Allen, Harper)
  Set Theory (Howe)
  Recursive Realizability (Troelstra)
  Frege Structures (Aczel)
  Denotational Semantics (Rezus)
• Understand KML type theoretically
• REason about KML programs in Nuprl
  Ensemble verification project

Record Encoding

• KML record
  
• Encode in type theory as a function mapping field names to data
  
  if then
  else if then
  else
• Dependent type

Type-Directed Compilation

• Past compilers stripped out the types
  Discards useful information
• Use type information for efficient compilation
  TIL compiler
  Tag-free garbage collection
  Subtyping elimination

KML

• Language design (clean)
• Type checking algorithm
  type reconstruction heuristic
• Semantics
  object encoding
  subtyping
  partial functions
  impredicativity
  control &effects
• Implementation

KML Implementation

• 20,000 lines of Caml-Light
• Caml-Light back-end
  soon to be using TIL
• Still to do:
  a few language features
  bootstrapped version
  debugger and other tools

Related Work (or, the competition)

• Objective CAML (INRIA)
• Pict (Pierce and Turner)
• Standard ML 1996 (Stone and Harper)

Conclusion

• Underlying philosophy:
  View Programming languages as a tractable approximation to foundational type theory
• Try to understand that approximation
  Type-theoretic semantics
• Try to mitigate the approximation
  Make programming languages more rich

• About this document ...