- to scale up by an order of magnitude the size of the problems we can deal with;
- to downsize by an order of magnitude the time needed for a given development.
To this end, we started studying a new version of the calculus of constructions in which user-defined computations expressed by rewrite rules can be made transparent in proof terms. In addition, this new calculus will come along with an internalized notion of parameterized module, allowing the user to build, store, retrieve and instantiate parameterized proofs. Finally, we intend to develop a platform dedicated to applications in telecommunications. After recalling what theorem provers and proof checkers are, we will give a short introduction to the calculus of constructions, its current limitations, before to briefly sketch the main ideas underlying our new calculus.