Universal algebra in type theory. (English) Zbl 0947.08001
Bertot, Yves (ed.) et al., Theorem proving in higher order logics. 12th international conference, TPHOLs ’99. Nice, France, September 14-17, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1690, 131-148 (1999).
Formalizing universal algebra within the theory of types by means of the proof development system Coq, the author sets up a framework for automated reasoning about general algebraic structures.
For the entire collection see [Zbl 0929.00038].
For the entire collection see [Zbl 0929.00038].
Reviewer: M.Armbrust (Köln)
MSC:
| 08A99 | Algebraic structures |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
| 08-04 | Software, source code, etc. for problems pertaining to general algebraic systems |
| 03B15 | Higher-order logic; type theory (MSC2010) |
