Specifications as data types

Explanation is the understanding-oriented part of the documentation. It may contain information about design decisions, alternatives, context and related works.

Contents

• Practical recommendations
  • Basic outline of programming language’s (static) semantics specification
  • Encoding functions and predicates and why you might not want to
  • Fortunate and unfortunate orderings of generators
  • Names vs. de Brujin indices
  • List- vs. SnocList-like representation of programs
  • Boolean vs. type-level predicates
  • Other thoughts and questions
• Experiments
  • Constructors
  • Arguments
  • Givens vs Pairs
  • Conclusion