proofs/typesystems

[Francois-Rene Rideau]

On Mon, Feb 22, 1999 at 03:12:08PM -0800, Tril wrote:
> Where did you hear about doing proofs with typesystems?
The Curry-Hindley-Howard isomorphism
that identifies types with logical propositions and programs with proofs
and has been well-known for long, and is the very founding principle
of systems like Coq (http://coq.inria.fr).
Even without taking this extreme position,
the use of typesystems, and more generally static program analyzes,
to automatically prove properties of programs (themselves to be used
in verifiers, optimizers, and other metaprograms)
is the basic motivation behind abstract interpretation
(see all papers that cite Cousot&Cousot 1977).

> If there is a type A, with subtypes B and C, but B and C do not overlap,
> and (B union C) is equal to A, [...]
The core of Coq does not use implicit subtyping
(well, Coq does have syntactic sugar for implicit coercion),
but it allows for explicit disjoint unions of types as a particular case
of its basic type construction mechanism: inductive types.

[ "Faré" | VN: Уng-Vû Bân | Join the TUNES project!   http://www.tunes.org/  ]
[ FR: François-René Rideau | TUNES is a Useful, Nevertheless Expedient System ]
[ Reflection&Cybernethics  | Project for  a Free Reflective  Computing System ]
Science is a process based on an attitude of logic, imagination and doubt.