Level: L3, M1
Contact: Burkhart Wolff<burkhart.wolff [at] universite-paris-saclay [dot] fr>, Idir Ait-Sadoune<idir.aitsadoune@centralesupelec.fr>
Location: Laboratoire Méthodes Formelles, Université Paris-Saclay
Keywords: Isabelle/HOL, Isabelle/DOF, Formal Document Generation
More Details: here
Context
Isabelle/DOF is a framework inside the Isabelle/HOL allowing to write technical reports, scientific papers, deliverables for certification processes, etc, so generally speaking: for documents that contain both formal and informal content. The linking between both is notoriously difficult, especially if both the formal and informal content is evolving during development. Roughly similar to Javadoc, Doxygen or ocamldoc, Isabelle/DOF allows for the integration of a kind of semantic macros (called antiquotations) into texts, λ-terms or code.
Isabelle/DOF extends the set of these antiquotations by a more general mechanism to *define* them via an ontology. For example, it is possible to define a domain ontologie from a software-engineering standard providing concepts like "definitions of a term", "requirements", "model-elements" and "test-results", etc. In a document conform to this ontology, a text element can be "tagged" as "safety_requirement".
Many features in Isabelle/DOF allow for writing even scientific papers and generating the LaTeX in a quality sufficient for conference [1,2,3]and journal publications [4,5]. While a Reference Manual describing the features on a technical level exists Isabelle/DOF User Manual vs. 1.1 (see the git for more recent versions), but this document is feature-oriented and not solution oriented as writers of documents need to find fast. Many LaTeX-snippets in the internet show how problem-oriented examples can substantially increase the usability of an advanced typesetting system.
Objectives
The purpose of this stage is to develop another Isabelle/DOF document which is a true "User Manual" in this sense. The result should be a generated .pdf and html - document organized in a "HowTo" - style for users, albeit still mechanically checked and tested against the (continuously evolving since under development) Isabelle/DOF system.
Requirements
- Good functional programming skills
- Skills in using LaTeX
- An Interest in advanced document modelling and processing
- Good and critic sense for communication to end-users
Supervision
- Burkhart Wolff, Professeur Université Paris-Saclay (burkhart.wolff@universite-paris-saclay.fr) et
- idir Ait-Sadoune, Maître de conférences Centrale Supelec (idir.aitsadoune@centralesupelec.fr).
References
[1] Achim D. Brucker, Burkhart Wolff: Using Ontologies in Formal Developments Targeting Certification. IFM 2019: 65-82
[2] Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Using Deep Ontologies in Formal Software Engineering. ABZ 2023: 15-32
[3] Safouan Taha, Burkhart Wolff and Lina Ye: Philosophers may dine - definitively ! iFM, Oct 2019.
[4] Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Modeling and analysing Cyber-Physical Systems in HOL-CSP. Robotics Auton. Syst. 170: 104549 (2023)
[5] Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Order-Sorted Polymorphisc Ontologies with an Application to Formal Software Engineering. submitted to SCP 2024.
[6] Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff:The Isabelle/DOF development git