Dimension 1: Design

Logical Frameworks encode

§Safety Proof
Languages

§Type Systems

§Security
Protocols

Benefit:

§Storing

§Shipping

§Checking

Proof Checker

Safety Proof

Safety Proof Language

Binary

Proof Checker

Safety Proof

Safety Proof Language

Binary

Proof Checker

Safety Proof Language

Safety Proof

Logical
Framework