Description
From a proof-theoretic perspective, Imandra's logic is effectively a typed version of PRA (Skolem's Primitive Recursive Arithmetic) extended with Transfinite Induction up to the ordinal epsilon_0.
It's a multisorted first-order logic, but Imandra has various niceties that allow it to handle a 'specializable' fragment of Higher-Order Logic
Since in Imandra everything is a program, all judgments are computational and because we live in a quantifier-free world of discrete combinatorial structures, we can admit classical logic and still obtain results that are constructively valid
In Imandra's logic all functions must be total and terminating, extension to the logic are accepted via defining new types or functions validated by Imandra's definitional principle, which analyses definitions to ensure they are admissible, to ensure that any extension by definitions is a conservative extension.
For exception-raising functions like List.hd, List.tl and /, Imandra has a semantics that under-specifies them, allowing them to take on any value in their 'exceptional' cases