Using Type Theory

  • Jean-François Monin
  • Michael G. Hinchey


In the table example, we would like to consider the search criterion P as a parameter. This is not possible in the framework of a formal method based on first-order logic, at least not in a satisfactory manner:
  • P may be encoded in the form of a set, but in the framework of B, for example, only certain finite sets are allowed;

  • Z is more flexible, but no straightforward mechanism is provided for deriving a program from the specification;

  • the axiom for search, in the algebraic specification of Chapter 10 is actually a schema of axioms; we then have to write down an instance of this schema for every property of interest.


Formal Method Type Theory Proof Obligation Proof Assistant Inductive Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London 2003

Authors and Affiliations

  • Jean-François Monin
    • 1
  • Michael G. Hinchey
    • 2
  1. 1.France Télécom R&D, Technopole AnticipaDTL/TALLannionFrance
  2. 2.Software Verification Research CentreUniversity of QueenslandBrisbaneAustralia

Personalised recommendations