Nominal Isabelle provides powerful tools for meta-theoretic reasoning
about syntax of logics or programming languages, in which variables are
bound. It has been instrumental to major verification successes, such as
Gödel’s incompleteness theorems. However, the existing tooling is not
compositional. In particular, it does not support nested recursion,
linear binding patterns, or infinitely branching syntax. These
limitations are fundamental in the way nominal datatypes and functions
on them are constructed within Nominal Isabelle. Taking advantage of
recent theoretical advancements that overcome these limitations through
a modular approach using the concept of map-restricted bounded natural
functor (MRBNF), we develop and implement a new definitional package for
binding-aware datatypes in Isabelle/HOL, called MrBNF. We describe the
journey from the user specification to the end-product types, constants
and theorems the tool generates. We validate MrBNF in two formalization
case studies that so far were out of reach of nominal approaches: (1)
Mazza’s isomorphism between the finitary and the infinitary affine
λ-calculus, and (2) the POPLmark 2B challenge, which involves non-free
binders for linear pattern matching.
This paper is a contribution to the meta-theory of systems featuring
syntax with bindings, such as 𝜆-calculi and logics. It provides a
general criterion that targets inductively defined rule-based systems,
enabling for them inductive proofs that leverage Barendregt’s variable
convention of keeping the bound and free variables disjoint. It improves
on the state of the art by (1) achieving high generality in the style of
Knaster–Tarski fixed point definitions (as opposed to imposing syntactic
formats), (2) capturing systems of interest without modifications, and
(3) accommodating infinitary syntax and non-equivariant predicates.
Formal reasoning about the time complexity of algorithms and data
structures is usually done in interactive theorem provers like
Isabelle/HOL. This includes reasoning about amortized time
complexity which looks at the worst case performance over a
series of operations. However, most programs are not written
within a theorem prover and thus use the data structures of the
production language. To verify the correctness it is necessary to
translate the data structures from the production language into the
language of the prover. Such a translation step could introduce errors,
for example due to a mismatch in features between the two languages.
We show how to prove amortized complexity of data structures directly
in Haskell using LiquidHaskell. Besides skipping the translation step,
our approach can also provide a didactic advantage. Learners do not have
to learn an additional language for proofs and can focus on the new
concepts only. For this paper, we do not assume prior knowledge of
amortized complexity as we explain the concepts and apply them in our
first case study, a simple stack with multipop. Moving to more
complicated (and useful) data structures, we show that the same
technique works for binomial heaps which can be used to implement a
priority queue. We also prove amortized complexity bounds for Claessen’s
version of the finger tree, a sequence-like data structure with
constant-time cons/uncons on either end. Finally we discuss the current
limitations of LiquidHaskell that made certain versions of the data
structures not feasible.
- David Messmann
- Thomas Grübler
- Felipe De Souza Nogueira Coelho
- Thorsten Ohlenforst
- Jan van Brügge
- + 12 more
MOVE-II (Munich Orbital Verification Experiment) will be the first
CubeSat of the Technical University of Munich (TUM) utilizing a
magnetorquer-based active attitude determination and control system
(ADCS). The ADCS consists of six circuit boards (five satellite side
panels and one central circuit board in satellite stack), each equipped
with a microcontroller, sensors and an integrated coil. The design
enables redundancy and therefore forms a fault-tolerant system with
respect to sensors and actuators. The paper describes the hardware
implementation, algorithms, software architecture, and first test
results of the integrated ADCS on the engineering unit. A possibility to
upgrade and extend our software after launch will enable further
research on new and innovative attitude determination and control
strategies and distributed computation on satellites. The MOVE-II flight
unit is in the integration and test phase with an intended launch date
in early 2018.