We describe a case-study of the application of webtechnology (Helm [2]) to create web-based didactic material out of a repository of formal mathematics (C-CoRN [5]), using the structure of an existing course (IDA [4]). The paper discusses the difficulties related to associating notation to a formula, the embedding of formal notions into a document (the "view"), and the rendering of proofs. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Asperti, A., Geuvers, H., Loeb, I., Mamane, L. E., & Coen, C. S. (2006). An interactive algebra course with formalised proofs and definitions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3863 LNAI, pp. 315–329). https://doi.org/10.1007/11618027_21
Mendeley helps you to discover research relevant for your work.