Squirrel
  • Introduction

Reference manual

  • Notations
    • Lexical conventions
      • Infix operators
  • Logic
    • Types
      • Base types
      • Type variables and polymorphism
      • General types
      • Binders and tags
    • Terms
      • Terms with binders
    • Multi-terms
      • Diff-terms
      • Macros
    • Formulas
      • Local formulas
      • Global formulas
  • Declarations
    • Terms
      • Names
      • Abstract functions
      • Operators
        • Built-ins
      • Cryptographic functions
    • Processes
      • Channels
      • Memory cells
      • Processes
      • Systems and actions
        • System-defined macros
        • System expressions
        • System contexts
    • Axioms and Lemmas
  • Proofs
    • Judgements
      • Logical variables
      • Hypotheses
      • Local judgement
      • Global judgement
    • Generalities
      • Tactic arguments
        • Intro patterns
      • Proof terms
        • Proof-term resolution
      • Reduction
      • Automatic simplification tactics
      • Tactics
      • Common errors
    • Tactics
      • Generic tactics
        • Common tactics
        • Local tactics
        • Global tactics
      • Structural tactics
        • Common tactics
        • Local tactics
        • Global tactics
      • Cryptographic tactics
        • Occurrence formula
        • Common tactics
        • Local tactics
        • Global tactics
      • Utility tactics
  • Commands

Tutorial

  • Protocol modelling
    • Messages
    • Basic assumption
    • Cryptographic assumptions
    • Protocols
  • Reachability properties
    • Macros
    • Formulas
  • Equivalence properties

Appendix

  • Indexes
    • Glossary index
    • Declaration index
    • Command index
    • Tactic index
    • Errors and warnings index
    • Index
  • Documenting Squirrel with Sphinx
    • TODO list generation
    • Squirrel objects
      • Notations
      • Objects
    • Squirrel directives
    • Squirrel roles
    • Common mistakes
      • Improper nesting
      • Overusing :token:
      • Omitting annotations
      • Using the .. squirreltop:: directive for syntax highlighting
      • Overusing plain quotes
      • Overusing the example directive
    • Tips and tricks
      • Nested lemmas
      • Abbreviations and macros
      • Advanced uses of notations
  • Bibliography
Squirrel
  • Search

© Copyright 2023, Squirrel developpers.

Built with Sphinx using a theme provided by Read the Docs.