About
Creator of Unit-B and Literate Unit-B.
My focus is specification, design, and…
Experience
Education
Volunteer Experience
-
Contributor
Haskell open source community
- Present 9 years 4 months
Science and Technology
Uploaded existential package to Hackage: links existential types and lenses
Preparing the axiomatic-testing package: uses QuickCheck to formulate and test type class axioms -
Verification Expert
OpenStack
- Present 9 years 3 months
Science and Technology
Presenting at OpenStack Summit - April 2016
-
-
-
Instructor
ETH Zurich
- Present 15 years
Education
Volunteer teaching: Program Derivation - Bernhard Brodowsky
-
Maintainer and Contributor
Lean Prover Community
- Present 6 years 4 months
Science and Technology
Publications
-
Sealing Pointer-Based Optimizations Behind Pure Functions
ArXiv.org
Set to be presented at ACM SIGPLAN International Conference on Functional Programming 2020
Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a higher-order combinator, and backtracking is dramatically simplified by persistent datastructures. However, existing \emph{pure} functional programming languages…Set to be presented at ACM SIGPLAN International Conference on Functional Programming 2020
Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a higher-order combinator, and backtracking is dramatically simplified by persistent datastructures. However, existing \emph{pure} functional programming languages all suffer a major limitation in these domains: traversing a term requires time proportional to the tree size of the term as opposed to its graph size. This limitation would be particularly devastating when building automation for interactive theorem provers such as Lean and Coq, for which the exponential blowup of term-tree sizes has proved to be both common and difficult to prevent. All that is needed to recover the optimal scaling is the ability to perform simple operations on the memory addresses of terms, and yet allowing these operations to be used freely would clearly violate the basic premise of referential transparency. We show how to use dependent types to seal the necessary pointer-address manipulations behind pure functional interfaces while requiring only a negligible amount of additional trust. We have implemented our approach for the upcoming version (v4) of Lean, and our approach could be adopted by other languages based on dependent type theory as well.Other authorsSee publication -
Data Types as Quotients of Polynomial Functors
10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA
A broad class of data types, including arbitrary nestings of inductive types, coinductive types, and quotients, can be represented as quotients of polynomial functors. This provides perspicuous ways of constructing them and reasoning about them in an interactive theorem prover.
Other authors -
-
The Unit-B Method — Refinement Guided by Progress Concerns
Software and Systems Modeling
We present Unit-B, a formal method inspired by Event-B and UNITY. Unit-B aims at the stepwise design of software systems, satisfying safety and liveness properties. The method features the novel notion of coarse and fine schedules, a generalisation of weak and strong fairness for specifying events’ scheduling assumptions. Based on events schedules, we propose proof rules to reason about progress properties and a refinement order preserving both liveness and safety properties. We illustrate our…
We present Unit-B, a formal method inspired by Event-B and UNITY. Unit-B aims at the stepwise design of software systems, satisfying safety and liveness properties. The method features the novel notion of coarse and fine schedules, a generalisation of weak and strong fairness for specifying events’ scheduling assumptions. Based on events schedules, we propose proof rules to reason about progress properties and a refinement order preserving both liveness and safety properties. We illustrate our approach by an example to show that systems development can be driven by not only safety but also liveness requirements.
Other authorsSee publication -
TTM/PAT: Specifying and Verifying Timed Transition Models
Springer
Timed Transition Models (TTMs) are event-based descriptions for specifying real-time systems in a discrete setting. We propose a convenient and expressive event-based textual syntax for TTMs and a corresponding operational semantics using labelled transition systems. A system is specified as a composition of module instances. Each module has a clean interface for declaring input, output, and shared variables. Events in a module can be specified, individually, as spontaneous, fair or real-time…
Timed Transition Models (TTMs) are event-based descriptions for specifying real-time systems in a discrete setting. We propose a convenient and expressive event-based textual syntax for TTMs and a corresponding operational semantics using labelled transition systems. A system is specified as a composition of module instances. Each module has a clean interface for declaring input, output, and shared variables. Events in a module can be specified, individually, as spontaneous, fair or real-time. An event action specifies a before-after predicate by a set of (possibly non-deterministic) assignments and nested conditionals. The TTM assertion language, linear-time temporal logic (LTL), allows references to event occurrences, including clock ticks (thus allowing for a check that the behaviour is non-Zeno). We implemented a model checker for the TTM notation (using the PAT framework) that includes an editor with static type checking, a graphical simulator, and a LTL verifier. The tool automatically derives the tick transition and implicit event clocks, removing the burden of manual encoding them. The TTM tool performs significantly better on a nuclear shutdown system than the manually encoded versions analyzed.
Other authors -
Systems Design Guided by Progress Concerns
Integrated Formal Methods
We evolved Event-B into Unit-B by using the UNITY logic. We apply Unit-B to the design of a control system similar to the one presented in "Development of Control Systems Guided by Models of their Environment" and by following the refinement strategy of first modelling the environment to be controlled, then modelling the actuators, then the sensors and finally the controller that use the previous two. The major difference is that, instead of leaving liveness consideration to be tackled at the…
We evolved Event-B into Unit-B by using the UNITY logic. We apply Unit-B to the design of a control system similar to the one presented in "Development of Control Systems Guided by Models of their Environment" and by following the refinement strategy of first modelling the environment to be controlled, then modelling the actuators, then the sensors and finally the controller that use the previous two. The major difference is that, instead of leaving liveness consideration to be tackled at the last stage, i.e. when it's possibly to late to ensure liveness, liveness is our first and guiding consideration throughout the development.
Other authors -
-
Development of Control Systems Guided by Models of their Environment
Electronic Notes in Theoretical Computer Science Volume 280, 14 December 2011, Pages 57–68
We used Event-B to refine a model of a train system while proving a series of safety properties (e.g. no collision between the trains). It eventually allowed us to deduce the relation between the inputs of the computer system and its output that ensures the safety of the system.
Other authors -
Courses
-
Computability and Decidability - lobbied for the course to run (2 students)
-
-
Concept of Object Oriented Programming - Peter Müller
-
-
Concurrent Object Oriented Programming - Bertrand Meyer
-
Honors & Awards
-
Ontario Graduate Scholarship
Province of Ontario
-
Queen Elizabeth II
Province of Ontario
-
NSERC Undergraduate Research Scholarship
Canadian Government
Languages
-
French
Native or bilingual proficiency
-
English
Native or bilingual proficiency
-
German
Elementary proficiency
Organizations
-
Comotion Coworking
-
- Present
Explore collaborative articles
We’re unlocking community knowledge in a new way. Experts add insights directly into each article, started with the help of AI.
Explore MoreOthers named Simon Hudon
2 others named Simon Hudon are on LinkedIn
See others named Simon Hudon