The French School of Programming

Foreword
Preface: The French School of Programming
Contents
About the Authors
1 The French School of Programming: A Personal View
	1.1 Parts, Chapters, and Authors
		1.1.1 Part I: Software Engineering
		1.1.2 Part II: Programming Language Mechanisms and Type Systems
		1.1.3 Part III: Theory
		1.1.4 Part IV: Language Design and Programming Methodology
	1.2 A Bit of Personal History
		1.2.1 One Is Never Safe from a Stroke of Luck
Part I Software Engineering
	2 ``Testing Can Be Formal Too'': 30Years Later
		2.1 Introduction
		2.2 Initial Set of Results: Testing Based on Algebraic Data Types
			2.2.1 Characteristics of This Kind of Specification
			2.2.2 Basic Principles of the Testing Method
			2.2.3 Tools
			2.2.4 Comparison with Previous Works
			2.2.5 Challenge and Solutions: Oracle and Observability
		2.3 Generalisation to Other Formal Specifications Methods
			2.3.1 LOTOS
				2.3.1.1 Characteristics of LOTOS
				2.3.1.2 Testability and Exhaustivity
				2.3.1.3 Formal Specifications of Processes with Inputs, Outputs and Data Types
			2.3.2 CSP
				2.3.2.1 Characteristics of CSP
				2.3.2.2 CSP Based Testing CavalcantiG07
			2.3.3 Circus
				2.3.3.1 Characteristics of Circus
				2.3.3.2 Circus Based Testing CavalcantiG11
				2.3.3.3 A Test Generation Tool for Circus: HOL-TestGen/Cirta Feliachi12,FeliachiGWW13
		2.4 Outcomes of Some Experiments
		2.5 Subsequent Works Along the Same Line
			2.5.1 VDM
			2.5.2 Object-Oriented Systems
				2.5.2.1 Ada and Object Oriented Programs
				2.5.2.2 ASTOOT and TACCLE
			2.5.3 HOL/TestGen
		2.6 Conclusion
		Appendix: Some Hints on the MAGGALY Experiment
		References
	3 A Short Visit to Distributed Computing Where Simplicity Is Considered a First Class Property
		3.1 Introduction
			3.1.1 University Professor: What Does It Mean? A Personal View
			3.1.2 Content
			3.1.3 Distributed Computing
		3.2 Causal Message Delivery
			3.2.1 A Causality-Related Problem
			3.2.2 A Very Simple Algorithm
		3.3 Causality-Related Issues in Distributed Checkpointing
			3.3.1 On the Consistency of Distributed Global States
			3.3.2 Z-dependency: Zigzag Paths and z-Cycles
			3.3.3 A Few Results on Distributed Checkpointing: Two Theorems
		3.4 A Visit to Read/Write Registers
			3.4.1 Atomic Read/Write Register
			3.4.2 Read/Write Registers in Crash-Prone Distributed Systems
			3.4.3 Read/Write Registers in the Presence of Byzantine Failures
		3.5 A Fundamental Need: To Agree and Cooperate
			3.5.1 Read/Write Registers Are Not Universal in Asynchronous Crash-Prone Message Passing Systems
			3.5.2 Consensus: A Fundamental Object
			3.5.3 Bad News and Good News
			3.5.4 The Condition-Based Approach
			3.5.5 The Case of Byzantine Processes
		3.6 Miscellaneous: There Is No End to Research
			3.6.1 Symmetry Breaking
			3.6.2 Anonymous Memory
			3.6.3 Fully Anonymous Systems
			3.6.4 Self-stabilization
		3.7 By Way of Conclusion
		Remark
		References
	4 Modeling: From CASE Tools to SLE and Machine Learning
		4.1 Introduction
		4.2 First Generation: CASE Tools
			4.2.1 The Idea
			4.2.2 The Good
			4.2.3 The Bad and the Ugly
		4.3 The Time of Model Driven Architecture (MDA)
			4.3.1 The Idea
			4.3.2 The Good
			4.3.3 The Bad and the Ugly
		4.4 Separation of Concerns with Models, Aspects and Features
			4.4.1 The Idea
			4.4.2 The Good
			4.4.3 The Bad and the Ugly
		4.5 Domain Specific Languages and Software Language Engineering
			4.5.1 The Idea
			4.5.2 The Good
			4.5.3 The Bad and the Ugly
		4.6 A New Challenge: Models and Data
		References
	5 At the Confluence of Software Engineeringand Human-Computer Interaction:A Personal Account
		5.1 Introduction
		5.2 Pre-HCI: Hardware Driven Interaction
		5.3 Seminal HCI: Graphical Interaction
			5.3.1 Graphical Interaction, Visual Metaphors and Direct Manipulation
			5.3.2 Cognitive Psychology: Micro- and Macro-theories Informing Software Tools
				5.3.2.1 Two Examples of Influential Micro-theory and Model: Gestalt Theory and Fitts' Law
				5.3.2.2 Two Examples of Influential Macro-theories: The “Seven Stages of Action” Model and the Model Human Processor
			5.3.3 Task Modeling Informing User Interface Design and Automatic Generation
			5.3.4 Usability as User-Centered Properties
				5.3.4.1 Interaction Flexibility
				5.3.4.2 Interaction Robustness
			5.3.5 Software Architecture Modeling for Interactive Systems
				5.3.5.1 Arch/Slinky: A Layered Architectural Approach to User Interface Functions
				5.3.5.2 MVC and PAC: Two Examples of a Distributed Architectural Approach for User Interface Functions
		5.4 Ubiquitous HCI: Embodied Interaction
			5.4.1 Tangible Interaction and Augmented Reality
				5.4.1.1 Tangible User Interfaces: Physical Objects as Input and Output Devices
				5.4.1.2 Augmented Reality: Incorporating Computation into the Real World
			5.4.2 Context-Aware Interaction and UI Plasticity
			5.4.3 End-User Development
		5.5 Conclusion
		References
Part II Programming Language Mechanisms and Type Systems
	6 From Procedures, Objects, Actors, Components, Services,to Agents
		6.1 Introduction
		6.2 Related Work
		6.3 Analysis
		6.4 Action Selection
		6.5 Coupling Flexibility
			6.5.1 Structural Coupling
			6.5.2 Communication Coupling
				6.5.2.1 Designation of the Receiver
				6.5.2.2 Data Transfer
				6.5.2.3 Temporal Coupling (Synchronization)
		6.6 Abstraction Level
			6.6.1 From Data to Concepts
			6.6.2 Reification
			6.6.3 Interoperability Languages
			6.6.4 Organizational Design
		6.7 Conclusion
		References
	7 Semantics and Syntax, Between Computer Scienceand Mathematics
		7.1 How I Became a Computer Scientist
		7.2 Various Flavours of Semantics
		7.3 The Full Abstraction Problem
		7.4 Sequential Algorithms
		7.5 The Categorical Abstract Machine
		7.6 Curry-Howard
		7.7 Dualities
		7.8 The Homotopical Era
		7.9 The French Touch in Semantics of Programs and Proofs
		References
	8 Some Remarks About Dependent Type Theory
		8.1 Introduction
		8.2 General Motivations and Context
			8.2.1 System F
			8.2.2 The System AUTOMATH
			8.2.3 Representation of Mathematical Notions in AUTOMATH
		8.3 AUTOMATH and System Fω
			8.3.1 Some Remarks
			8.3.2 Russell-Prawitz Encoding of Logical Connectives
			8.3.3 Encoding of Data Types
			8.3.4 Evaluation and Comparison with Other Formal Systems
				8.3.4.1 Decidable Type Checking
				8.3.4.2 Impredicativity in Logic and Functional System
				8.3.4.3 Comparison with Frege's Begriffsschrift
		8.4 Inductive Definitions and Data Types
		8.5 Consistency and Paradoxes
			8.5.1 Girard's Paradox
			8.5.2 Parametricity and Normalisation Proofs
		8.6 Consistency and Expressiveness
		8.7 Intensional Expressiveness and Inductive Definitions
		Conclusion
		Appendix
		References
Part III Theory
	9 A Personal Historical Perspective on Abstract Interpretation
		9.1 Origin
		9.2 Widening
		9.3 Example of Widening (and Narrowing)
		9.4 From Flowcharts to Structural Induction
		9.5 Bibliographic Input
		9.6 Soundness and Termination Proof
		9.7 Initial Publication
		9.8 Development of the Theory from an Algorithmic to an Algebraic Framework
		9.9 Narrowing
		9.10 Fixpoints
		9.11 Verification
		9.12 Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints
		9.13 Recursion and Modularity
		9.14 Chaotic and Asynchronous Iterations
		9.15 Types
		9.16 Galois Connections, Closures, Moore Families, Etc.
		9.17 Transition Systems
		9.18 Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes
		9.19 Automatic Discovery of Linear Restraints Among Variables of a Program
		9.20 Systematic Design of Program Analysis Frameworks
		9.21 Parallelism
		9.22 Proof Methods and Induction Principles
		9.23 Back to Static Analysis
		9.24 A Variety of Abstract Interpretation Models
		9.25 Language Independence
		9.26 Bi-inductive Definition of Maximal Traces
		9.27 Hierarchies of Semantics
		9.28 Calculational Design
		9.29 Calculational Design of Abstract Semantics
		9.30 Calculational Design of Algorithms
		9.31 Static Analysis Is Harder than Verification
		9.32 The Origin of Astrée
		9.33 Astrée
		9.34 Applications
		9.35 Introductions, Surveys, Reports, and Prospective Discussion Texts
		9.36 Conclusion
		References
	10 Tracking Redexes in the Lambda Calculus
		10.1 Introduction
		10.2 Preliminaries
		10.3 The Labeled Lambda-Calculus
		10.4 Labels and Permutation Equivalence
		10.5 The History of Redexes
		10.6 Other Calculi
		10.7 Conclusion
		References
	11 Confluence of Terminating Rewriting Computations
		11.1 Introduction
		11.2 Terminating Computations on First-Order Terms
			11.2.1 Abstract Church-Rosser Properties of Plain Rewriting
			11.2.2 Confluence of Terminating Plain Rewriting
		11.3 Terminating Computations on Congruence Classes of Terms
			11.3.1 Abstract Church-Rosser Modulo
			11.3.2 Rewriting Modulo
			11.3.3 Church-Rosser Properties of Rewriting Modulo
		11.4 Terminating Computations on Higher-Order Terms
			11.4.1 Terms
			11.4.2 Substitutions
			11.4.3 Splitting and Sticking
			11.4.4 Reductions
			11.4.5 Functional Reductions
			11.4.6 Higher-Order Reductions
			11.4.7 Higher-Order Rewrite Systems
			11.4.8 Typed Rewriting Structures
			11.4.9 Unification in Typed Rewriting Structures
		11.5 Church-Rosser Properties of Typed Rewriting Structures
			11.5.1 Plain Typed Rewriting Structures
			11.5.2 Terminating Typed Rewriting Structures Modulo
		11.6 Two Examples of Application to Programming Languages
			11.6.1 Maude
			11.6.2 Dedukti
		11.7 Conclusion
		References
Part IV Language Design and Programming Methodology
	12 Programming with Union, Intersection, and Negation Types
		12.1 Introduction
		12.2 Motivations
		12.3 Types
			12.3.1 Limitations of Syntactic Systems
			12.3.2 Semantic Subtyping
			12.3.3 Polymorphic Extension
		12.4 Languages
			12.4.1 Theoretical Framework
				12.4.1.1 On Deriving Negation Types
				12.4.1.2 On the Feasibility of Type-Inference
				12.4.1.3 Practical Systems
			12.4.2 Core CDuce
				12.4.2.1 Closing the Circle
				12.4.2.2 Inferring Intersection Types for Functions
				12.4.2.3 Type-Cases
				12.4.2.4 Random Choice
				12.4.2.5 Polymorphic Language
			12.4.3 An Implicitly-Typed Polymorphic Language with Set-Theoretic Types
				12.4.3.1 Type Reconstruction
				12.4.3.2 Adding Type Annotations
				12.4.3.3 A Remark on Occurrence Typing
			12.4.4 Occurrence Typing and Reconstruction of Intersections
			12.4.5 Summary
		12.5 Further Features
			12.5.1 Pattern Matching
			12.5.2 Gradual Typing
			12.5.3 Denotational Semantics
		12.6 Conclusion
		Appendix: Core Calculus of CDuce FCB08
			Syntax
			Reduction Semantics
			Type-System
		References
	13 Right and Wrong: Ten Choices in Language Design
		A Introduction
			A.1 Background
			A.2 Design Guidelines
			A.3 Discussion Style
			A.4 Language Criticism
			A.5 Scope
			A.6 The Role of the Type System
			A.7 Precise Object-Oriented Terminology
		B Mathematical Notations
			B.1 Functions
			B.2 Overriding Union
			B.3 Finite Permutations
		1 Uniform Access
			1.1 Computing, or Looking Up
			1.2 What Do We Do with Fields?
			1.3 Exporting Queries as Queries
			1.4 Getters and Setters
			1.5 Assigner Commands
		2 Dijkstra Was Right
		3 Overloading and Constructors
			3.1 Syntactic Overloading: An Example
			3.2 Semantic Overloading Through Polymorphism and Dynamic Binding
			3.3 Syntactic Overloading Is Useless and Harmful in an OO Context
			3.4 Overloaded Constructors
		4 Inheritance and Interfaces
			4.1 Redefinition
			4.2 Renaming
			4.3 Multiple Inheritance
			4.4 Interfaces
			4.5 Limitations of Interfaces in Pre-OO Modular Languages
			4.6 Programs with Holes
			4.7 Combining Abstractions
			4.8 Interfaces as Automatically Derived Artifacts
		5 Contract Mechanisms
			5.1 A Close Integration with the Language
			5.2 Class Invariants
			5.3 A Plethora of Run-Time Checks for Free
			5.4 At the Very Core of Inheritance Concepts
			5.5 Understanding the Design by Contract Methodology
			5.6 An Integral Part of the Approach
		6 Static Classes and Shared Information
			6.1 Class Methods and Static Classes
			6.2 Once Routines
			6.3 Instance-Free Features
			6.4 Varieties of Once Routines
		7 Old Syntax for New Semantics
			7.1 Aliases of Various Kinds
			7.2 Once Classes
			7.3 Iterators
			7.4 Conversions
			7.5 Unfolded Forms
			7.6 Agents and Functional-Style Programming
			7.7 About the Role of Agents: Functional Mechanisms in an OO Shell
		8 Exception Handling
			8.1 Modes of Exception Use
			8.2 A Clear Conceptual Framework for Exception Handling
			8.3 Eiffel Exception Mechanism
		9 Concurrency
			9.1 Semantic Mismatches
			9.2 An Example: What Happens to Preconditions?
			9.3 Sequential Versus Concurrent
			9.4 Simultaneous Resource Reservation
			9.5 Processors and Regions
			9.6 Synchrony, Asynchrony and Wait by Necessity
			9.7 Language Support
			9.8 Synchronization
		10 Void Safety
		Appendix A1: Language Description
		Appendix A2: Language Evolution
		Bibliography
		References