| Date: | 2022, April 26 |
| Time: | 10:30 a. m. |
| Place: | G29-018 |
| Author: | Mossakowski, Till |
| Title: | HasCASL: A Logic Combining Higher-Order Logic, Type Classes, Polymorphism, Subsorting and Partial Functions |
We lay out the design of HasCASL, a higher order extension of the algebraic specification language CASL that serves both as a wide-spectrum language for the rigorous specification and development of software, in particular but not exclusively in modern functional programming languages, and as an expressive standard language for higher-order logic. Distinctive features of HasCASL include partial higher order functions, higher order subtyping, shallow polymorphism, and an extensive type-class mechanism. Moreover, HasCASL provides dedicated specification support for monad-based functional-imperative programming with generic side effects, including a monad-based generic Hoare logic. This has been joint work with Lutz Schröder. The current interest in HasCASL is due to the wish for integration of theorem provers that can handle induction axioms into the Heterogeneous tool set Hets. One such prover features type classes, subtyping and polymorphism. Hence the interest in a logic that supports such features.