FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Lucas Interpretation from Programmers’ Perspective

Author: Walther Neuper

Paper Information

Title:Lucas Interpretation from Programmers’ Perspective
Authors:Walther Neuper
Proceedings:ThEdu Extended Abstracts
Editors: Pedro Quaresma and Walther Neuper
Keywords:proof assistant, Isabelle, function package, engineering mathematics, tutoring, lucas interpretation
Abstract:

ABSTRACT. Within the process of pushing the ISAC prototype towards maturity for service in engineering courses one of the most crucial points is to make programming convenient in ISAC . Programming means to describe mathematical algorithms (a functional program without input/output, so no concern with didactics and dialogues, which are handled by a separate component not discussed here) of engineering problems by use of libraries of methods and specifications as well as of respective theories. ISAC builds upon the theorem prover Isabelle, which offers a convenient programming environment and a specific function package. This is considered an appropriate means to improve programming in ISAC as required. The first steps of improvement are described in this paper and the other steps are listed in detail.

Pages:8
Talk:Jul 18 11:00 (Session 126M)
Paper: