ANR PML - Historique des versions

Raffalli : /* Context and positioning of the proposal */

2011-01-13T11:35:09Z

Context and positioning of the proposal

← Version précédente		Version du 13 janvier 2011 à 11:35
Ligne 25 :		Ligne 25 :
	proof match x with		proof match x with
	Z[] -> 8< (* trivial case handled automatically by Knuth-Bendix *)		Z[] -> 8< (* trivial case handled automatically by Knuth-Bendix *)


	\| S[x'] ->		\| S[x'] ->
	let _ = mul_associative x' y z in (* There is a syntactic sugar for that... *)		let _ = mul_associative x' y z in (* There is a syntactic sugar for that... *)

Thirs : /* Context and positioning of the proposal */

2011-01-13T11:34:25Z

Context and positioning of the proposal

← Version précédente		Version du 13 janvier 2011 à 11:34
Ligne 25 :		Ligne 25 :
	proof match x with		proof match x with
	Z[] -> 8< (* trivial case handled automatically by Knuth-Bendix *)		Z[] -> 8< (* trivial case handled automatically by Knuth-Bendix *)

	\| S[x'] ->		\| S[x'] ->
	let _ = mul_associative x' y z in (* There is a syntactic sugar for that... *)		let _ = mul_associative x' y z in (* There is a syntactic sugar for that... *)

Thirs : /* Context and positioning of the proposal */

2011-01-13T11:33:23Z

Context and positioning of the proposal

← Version précédente		Version du 13 janvier 2011 à 11:33
Ligne 7 :		Ligne 7 :
	Another orthogonal phenomenon is the emergence of formal methods used in conjunction with various programming languages to test, check or prove software. This introduces another layer to languages in order to write specifications, and sometimes yet another one for proofs. Learning a programming language together with the associated specification/proof languages can take an important effort.		Another orthogonal phenomenon is the emergence of formal methods used in conjunction with various programming languages to test, check or prove software. This introduces another layer to languages in order to write specifications, and sometimes yet another one for proofs. Learning a programming language together with the associated specification/proof languages can take an important effort.

	Projects such as [http://www.cs.utexas.edu/users/moore/acl2/ ACL2], the successor of [http://www.cs.utexas.edu/users/boyer/ftp/nqthm ~~nqthm,~~ the Boyer-Moore theorem prover] uses a rather simple language (namely LISP) both as a programming language and specification language, allowing to keep a unity in the system. Unfortunately, LISP is somewhat limited both as a programming language (no good treatment of sum ~~type~~, no module system) and a specification language (very limited quantification). Moreover, LISP has no compile-time type-checking, which has proved very useful to detect bugs and automatically assert properties.		Projects such as [http://www.cs.utexas.edu/users/moore/acl2/ ACL2], the successor of [http://www.cs.utexas.edu/users/boyer/ftp/nqthm the Boyer-Moore theorem prover] uses a rather simple language (namely LISP) both as a programming language and specification language, allowing to keep a unity in the system. Unfortunately, LISP is somewhat limited both as a programming language (no good treatment of sum types, no module system) and a specification language (very limited quantification). Moreover, LISP has no compile-time type-checking, which has proved very useful to detect bugs and automatically assert properties.

	The aim of ~~this~~ project is to build a very powerful language (with no loss of expressive power compared to state of the art languages) based on a very small number of simple features. We think this will be possible thanks to recent progress both in the semantics of programming languages and the apparition of new algorithms for type inference based on ~~constraints~~-solving. In fact, we propose in [RAF10b] an innovative concept derived from the later to enable this: ~~constraints~~-checking.		The aim of the present project is to build a very powerful language (with no loss of expressive power compared to state of the art languages) based on a very small number of simple features. We think this will be possible thanks to recent progress both in the semantics of programming languages and the apparition of new algorithms for type inference based on constraint-solving. In fact, we propose in [RAF10b] an innovative concept derived from the later to enable this: constraint-checking.

	Moreover, the language will be used not only as a programming language and a specification language (like in ACL2), but also as the proof language. This is natural for an ML-like language because pattern-matching is a natural and powerful way to make a proof by case analysis. This also means that our tool will ~~follow~~ ~~the ''KISS'' philosophy:~~ relatively few (unified) features, yet powerful.		Moreover, the language will be used not only as a programming language and a specification language (like in ACL2), but also as the proof language. This is natural for an ML-like language because pattern-matching is a natural and powerful way to make a proof by case analysis. This also means that our tool will consist of relatively few (unified) features, yet powerful.

	The idea of a new language arose from the discovery of a new typing algorithm [RAF10b] whose implementation gave birth to a first implementation of PML (Proved ML) by Christophe Raffalli. This implementation is already available from [http://www.lama.univ-savoie.fr/~pml the web page of the language]. However, turning PML into a real tool requires a lot of research and implementation work and this is why we request the help of the ANR. Some of the goals are highlighted in the next sections.		The idea of a new language arose from the discovery of a new typing algorithm [RAF10b] whose implementation gave birth to a first implementation of PML (Proved ML) by Christophe Raffalli. This implementation is already available from [http://www.lama.univ-savoie.fr/~pml the web page of the language]. However, turning PML into a real tool requires a lot of research and implementation work and this is why we request the help of the ANR. Some of the goals are highlighted in the next sections.


			'''PML approach to mathematics and program certification is unique''' Existing provers or certification tools feature a base programming language, and a logical layer on top of it (be it to write mathematical statements, specifications, or proofs). PML is very different in spirit: every statement, including sophisticated mathematical ones, is reduced to a statement asserting that a program fragment does not raise any error.
⚫	~~'''PML approach to proofs of specification is unique'''~~ PML has no dedicated proof language, but the user can still write proofs! Existing programming languages supporting specifications use two alternatives: automated proofs (ACL2, Why) or proof obligations that the user can prove using specific language (Coq extraction, Focalize, Why). Several systems provide both, ~~the~~ manual proofs being used only when automation fails. PML is very different ~~in spirit~~: it introduces a new instruction, written with a "scissors symbol" <tt>'''8<'''</tt> to express that the corresponding position in the program is ''dead'', meaning that it can not be reached during evaluation. This condition is checked by a terminating variant of the Knuth-Bendix completion algorithm. This is rather simple and therefore easier to trust than modern decision procedures. However, it only solves trivial cases: to write complex proofs, the user just uses the same syntax as for programs to do case analysis or induction (~~''ie~~.'' recursive definitions). This means that the user does not need learn a specific proof language and hopefully implies that PML is easier to learn and probably more adapted to industry that previous solutions.

		⚫	PML has no dedicated proof language, but the user can still write proofs! Existing programming languages supporting specifications use one or more of the following two alternatives: automated proofs (ACL2, Why) or proof obligations, that the user can prove using a specific language (Coq extraction, Focalize, Why). Several systems provide both possibilities, manual proofs being used only when automation fails. PML is again very different: it introduces a new instruction, written with a "scissors symbol" <tt>'''8<'''</tt> to express that the corresponding position in the program is ''dead'', meaning that it can not be reached during evaluation. This condition is checked by a terminating variant of the Knuth-Bendix completion algorithm. This is rather simple and therefore easier to trust than modern decision procedures. However, it only solves trivial cases: to write complex proofs, the user just uses the same syntax as for programs to do case analysis or induction (i.e., recursive definitions). This means that the user does not need learn a specific proof language and hopefully implies that PML is easier to learn and probably more adapted to industry that previous solutions.
⚫	The logic of PML is just the equational theory of its programming language; and we use variants of Knuth-Bendix completion as a proof-checker. The first experiments with the current implementation are promising. However, Knuth-Bendix procedure in the context of ML is a complex and new research problem. A lot more work is needed, for instance to handle proofs in arithmetic which occur quite often. Here is an example of a proof in arithmetic, checked in the current version of PML. This is not completely satisfactory (hard to write), but shows the use of the language for both proofs and programs and the use of recursive functions for inductive proofs:

		⚫	The logic of PML is just the equational theory of its programming language; and we use variants of Knuth-Bendix completion as a proof-checker. The first experiments with the current implementation are promising. However, adapting the Knuth-Bendix procedure to the context of ML is a complex and new research problem. A lot more work is needed, for instance to handle proofs in arithmetic which occur quite often. Here is an example of a proof in arithmetic, checked in the current version of PML. This is not completely satisfactory (hard to write), but shows the use of the language for both proofs and programs and the use of recursive functions for inductive proofs:

	val rec mul_associative x y z \|- (x * y) * z == x * (y * z)		val rec mul_associative x y z \|- (x * y) * z == x * (y * z)
Ligne 40 :		Ligne 42 :
	Moreover, this style of proof is declarative and relatively readable (like Mizar proofs) while concise at the same time. This is very important when you want to maintain large developments.		Moreover, this style of proof is declarative and relatively readable (like Mizar proofs) while concise at the same time. This is very important when you want to maintain large developments.

	'''PML is different from the other modern programming languages''' because its design focuses on a few powerful concepts. One consequence is that it is more difficult for a compiler to produce efficient code. In particular, since PML unifies several notions of products (modules, tuples and records), there is no simple way to choose the internal representation of a product, especially with implicit subtyping. Writing a good compiler for PML will thus require more complex and original optimization schemes (probably driven by typing) than languages like OCaml or Haskell. A Polish student (Wojciech Matyjewicz) is just starting a PhD on this very topic.		'''PML is different from the other modern programming languages''' because its design focuses on a few powerful concepts. One consequence is that it is more difficult for a compiler to produce efficient code. In particular, since PML unifies several notions of products (modules, tuples and records), there is no simple way to choose the internal representation of a product, especially with implicit subtyping. Writing a good compiler for PML will thus require more complex and original optimization schemes (probably driven by typing) than for languages like OCaml or Haskell. A Polish student (Wojciech Matyjewicz) is just starting a PhD on this very topic.

	Here is a simple example, accepted by the current version of PML, demonstrating product ~~type~~, sum ~~type~~ and subtyping. We define ternary trees as an extension of binary trees with an implicit subtyping		Here is a simple example, accepted by the current version of PML, demonstrating product types, sum types and subtyping. We define ternary trees as an extension of binary trees with an implicit subtyping
	relation (all functions accepting binary_trees will accept ternary trees, by ignoring the <tt>middle_son</tt>):		relation (all functions accepting binary_trees will accept ternary trees, by ignoring the <tt>middle_son</tt>):

Raffalli : /* Annexes */

2011-01-13T11:23:26Z

Annexes

← Version précédente		Version du 13 janvier 2011 à 11:23
Ligne 492 :		Ligne 492 :
	* [Raf10b] ''Realizability for programming languages'' (submitted, available as hal-00474043)		* [Raf10b] ''Realizability for programming languages'' (submitted, available as hal-00474043)

	* [Raf08a] ''PML and strong ~~normalisation~~'' conference at the Types workshop, April 2008, Turino, Italy		* [Raf08a] ''PML and strong normalization'' conference at the Types workshop, April 2008, Turino, Italy

	* [Raf07b] ''PML: a new proof assistant'' conference at the Types workshop, may 2007, Cividale del Friuli (Udine), Italy		* [Raf07b] ''PML: a new proof assistant'' conference at the Types workshop, may 2007, Cividale del Friuli (Udine), Italy
Ligne 744 :		Ligne 744 :
	* Christophe Raffalli is involved in the ANR proposal RÉCRÉ.		* Christophe Raffalli is involved in the ANR proposal RÉCRÉ.

	Remark: the interaction with PML and RÉCRÉ is natural because the proof technics used for ensuring some of the properties of the language PML is ~~réalizability~~ which is one of the théma of the ANR proposal RÉCRÉ.		Remark: the interaction with PML and RÉCRÉ is natural because the proof technics used for ensuring some of the properties of the language PML is realizability which is one of the théma of the ANR proposal RÉCRÉ.

Raffalli : /* Scientific justification of requested budget */

2011-01-13T11:22:04Z

Scientific justification of requested budget

← Version précédente		Version du 13 janvier 2011 à 11:22
Ligne 367 :		Ligne 367 :
	For instance, Andreas Abel came to visit Chambéry in 2010 for two weeks financed by our PEPS		For instance, Andreas Abel came to visit Chambéry in 2010 for two weeks financed by our PEPS
	project and during this time induced an important bootstrap to the implementation of the termination checker		project and during this time induced an important bootstrap to the implementation of the termination checker
	[Hyv10b] and contributed a non trivial example with a proved ~~implentation~~ of left-leaning red-black trees.		[Hyv10b] and contributed a non trivial example with a proved implantation of left-leaning red-black trees.

	We want to continue such interaction. Andreas Abel already agreed as well as Joe Wells for discusion about error reporting and , Assia Mahboubi for complex proofs involving the reflexion principle. Many other discussion would be profitable about PML runtime (with multithreading ?), interaction with external tools (termination checker or automated theorem prover),		We want to continue such interaction. Andreas Abel already agreed as well as Joe Wells for discusion about error reporting and , Assia Mahboubi for complex proofs involving the reflexion principle. Many other discussion would be profitable about PML runtime (with multithreading ?), interaction with external tools (termination checker or automated theorem prover),
Ligne 415 :		Ligne 415 :
	To be compared with the total of 104/112 month not payed by the ANR. We consider that this is a good balance.		To be compared with the total of 104/112 month not payed by the ANR. We consider that this is a good balance.

	~~Le coût~~ total ~~est~~ de 308589€.		The total cost is 308589€.

	====Human resources not financed by the ANR====		====Human resources not financed by the ANR====
Ligne 467 :		Ligne 467 :
	on the website.		on the website.

	~~Le coût~~ total ~~est~~ de 350333€ ~~snas ternir compte de~~ Christophe Mouilleron.		The total cost is 350333€, ignoring Christophe Mouilleron.

	==Annexes==		==Annexes==

Raffalli : /* Scientific and technical program, project management */

2011-01-13T11:19:37Z

Scientific and technical program, project management

Thirs : /* Tom Hirshowitz (LAMA, Chambéry) */

2011-01-13T11:16:08Z

Tom Hirshowitz (LAMA, Chambéry)

← Version précédente		Version du 13 janvier 2011 à 11:16
Ligne 623 :		Ligne 623 :
	1016--1027.		1016--1027.

	==== Tom ~~Hirshowitz~~ (LAMA, Chambéry) ====		==== Tom Hirschowitz (LAMA, Chambéry) ====

	34 ans, CR CNRS (informatique) , LAMA		34 ans, CR CNRS (informatique) , LAMA

Raffalli : /* Involvement of project participants to other grants, contracts, etc … */

2011-01-13T11:16:05Z

Involvement of project participants to other grants, contracts, etc …

← Version précédente		Version du 13 janvier 2011 à 11:16
Ligne 743 :		Ligne 743 :
	* Alexandre Miquel is involved in the ANR proposal RÉCRÉ.		* Alexandre Miquel is involved in the ANR proposal RÉCRÉ.
	* Christophe Raffalli is involved in the ANR proposal RÉCRÉ.		* Christophe Raffalli is involved in the ANR proposal RÉCRÉ.


	Remark: the interaction with PML and RÉCRÉ is natural because the proof technics used for ensuring some of the properties of the language PML is réalizability which is one of the théma of the ANR proposal RÉCRÉ.		Remark: the interaction with PML and RÉCRÉ is natural because the proof technics used for ensuring some of the properties of the language PML is réalizability which is one of the théma of the ANR proposal RÉCRÉ.

Raffalli : /* Involvement of project participants to other grants, contracts, etc … */

2011-01-13T11:15:58Z

Involvement of project participants to other grants, contracts, etc …

← Version précédente		Version du 13 janvier 2011 à 11:15
Ligne 738 :		Ligne 738 :
	===Involvement of project participants to other grants, contracts, etc …===		===Involvement of project participants to other grants, contracts, etc …===

	* Frederic Blanqui is involved in the Sino-French ANR SIVES 2009-2011 on SImulation and Verification based platform for developing Embedded Systems.
	* Emmanuel Chailloux is member of the ANR PWD ("Programmation du Web Diffus"), whose leader is Manuel Serrano (Inria), and the FUI [http://opengpu.net/ OpenGPU project].		* Emmanuel Chailloux is member of the ANR PWD ("Programmation du Web Diffus"), whose leader is Manuel Serrano (Inria), and the FUI [http://opengpu.net/ OpenGPU project].
	* Tom Hishowitz is involved in the ANR PiCoq the ANR proposals RÉCRÉ and CATHRE.		* Tom Hishowitz is involved in the ANR PiCoq the ANR proposals RÉCRÉ and CATHRE.

Raffalli : /* Scientific and technical description */

2011-01-13T11:15:32Z

Scientific and technical description

← Version précédente		Version du 13 janvier 2011 à 11:15
Ligne 60 :		Ligne 60 :

	The ML programming language, created by Robin Milner <em>et al</em> in the 80's has two major distinctive features:		The ML programming language, created by Robin Milner <em>et al</em> in the 80's has two major distinctive features:
	* Algebraic data-types and pattern matching: data types are basically all constructed using fixpoint, ~~cartesian~~ product (product types) and disjoint union (sum types).		* Algebraic data-types and pattern matching: data types are basically all constructed using fixpoint, Cartesian product (product types) and disjoint union (sum types).
	* Static type inference: the type of every piece of code is automatically inferred using Hindley-Milner algorithm (HM). By construction, once compiled, an ML program can not crash (no segmentation fault). More precisely, when we do not use unsafe features of the language (like interface with unsafe libraries written in C), if an ML program produces a segmentation fault, then there is a bug in the type-checker or the compiler.		* Static type inference: the type of every piece of code is automatically inferred using Hindley-Milner algorithm (HM). By construction, once compiled, an ML program can not crash (no segmentation fault). More precisely, when we do not use unsafe features of the language (like interface with unsafe libraries written in C), if an ML program produces a segmentation fault, then there is a bug in the type-checker or the compiler.

Ligne 69 :		Ligne 69 :
	* HM(X) does not completely solve the problem of subtyping. The language to express the types constructed by the constraint solver is the same as the language of types used by programmers. With constraints <math>\alpha \subseteq \beta</math> and <math>\alpha \subseteq \gamma</math> for three types <math>\alpha</math>, <math>\beta</math> and <math>\gamma</math>, the most natural solution is <math>\alpha = \beta \cap \gamma</math>. This implies that intersection needs to be part of the language for types. This means that constraints such as <math>\beta \cap \gamma \subseteq \delta</math> may also appear and they are problematic to deal with. Similar reasoning shows that constraints of the form <math>\beta \cap \gamma \subseteq \beta' \cup \gamma'</math> may appear, increasing the complexity of constraint solving by an exponential factor.		* HM(X) does not completely solve the problem of subtyping. The language to express the types constructed by the constraint solver is the same as the language of types used by programmers. With constraints <math>\alpha \subseteq \beta</math> and <math>\alpha \subseteq \gamma</math> for three types <math>\alpha</math>, <math>\beta</math> and <math>\gamma</math>, the most natural solution is <math>\alpha = \beta \cap \gamma</math>. This implies that intersection needs to be part of the language for types. This means that constraints such as <math>\beta \cap \gamma \subseteq \delta</math> may also appear and they are problematic to deal with. Similar reasoning shows that constraints of the form <math>\beta \cap \gamma \subseteq \beta' \cup \gamma'</math> may appear, increasing the complexity of constraint solving by an exponential factor.

	PML's approach is to replace type-inference by ''constraint <u>checking</u>'' rather than constraint solving: we only check that the constraints are ~~satisfiyable~~ in some model. Type-checking in the current implementation of PML can be seen as a black box ensuring that nothing can go wrong during execution. Moreover, since we do not need to write solutions for the constraints, the language for types can be relatively simple. In fact, the types written by the programmer aren't even the actual type constraints that are checked: they are syntactic sugar for the partial identity on the intended type (giving for free nice feature like higher-order parametric types, that is types with parameters which may be themselves types with parameters). In other words, the expression <tt>x:nat</tt> is a synonym for <tt>(id_nat x)</tt> where		PML's approach is to replace type-inference by ''constraint <u>checking</u>'' rather than constraint solving: we only check that the constraints are satisfiable in some model. Type-checking in the current implementation of PML can be seen as a black box ensuring that nothing can go wrong during execution. Moreover, since we do not need to write solutions for the constraints, the language for types can be relatively simple. In fact, the types written by the programmer aren't even the actual type constraints that are checked: they are syntactic sugar for the partial identity on the intended type (giving for free nice feature like higher-order parametric types, that is types with parameters which may be themselves types with parameters). In other words, the expression <tt>x:nat</tt> is a synonym for <tt>(id_nat x)</tt> where
	val rec id_nat x = match x with		val rec id_nat x = match x with
	Z[] -> Z[]		Z[] -> Z[]
Ligne 80 :		Ligne 80 :
	====Proof assistant====		====Proof assistant====

	Proof assistants have evolved rapidly since Automath in the 70th. Two main trends coexist: automated proof assistants such as ACL2, PVS and ''safe'' ones such as Coq, Isabelle, PhoX, Lego, HOL, Matita, <em>etc.</em> The former incorporate very sophisticated automated deduction strategies, with no ''certificate'' for the validity of the proof, while the later require all proofs to be done in a specific framework (like natural deduction or type theory) allowing for a simple check of the proof. The gap between the two approaches tend to be reduced by the emergence of complex tactics (for Coq or Isabelle mainly) which build proofs for the user. For instance Zenon is an advanced automated first-order theorem prover ~~outputing~~ a Coq proof.		Proof assistants have evolved rapidly since Automath in the 70th. Two main trends coexist: automated proof assistants such as ACL2, PVS and ''safe'' ones such as Coq, Isabelle, PhoX, Lego, HOL, Matita, <em>etc.</em> The former incorporate very sophisticated automated deduction strategies, with no ''certificate'' for the validity of the proof, while the later require all proofs to be done in a specific framework (like natural deduction or type theory) allowing for a simple check of the proof. The gap between the two approaches tend to be reduced by the emergence of complex tactics (for Coq or Isabelle mainly) which build proofs for the user. For instance Zenon is an advanced automated first-order theorem prover that outputs a Coq proof.

	The common defect of all these proof assistants is that a proof can not be written nor understood without running the proof assistant. Some proof assistants such as Mizar or Alf do not follow exactly the above scheme: Mizar has a declarative style for proof which is (in theory) readable by a human and checked by a limited checker (This proof style has been adapted to Coq and Isabelle). Unfortunately, there is no formal description of the Mizar proof checker. Alf on the other hand is based on proof theory and requires the user to basically write the complete proof tree just leaving out a few details. The logic is very well formalized and simple, but writing proof is tedious and not similar to the usual practice of informal mathematics.		The common defect of all these proof assistants is that a proof can not be written nor understood without running the proof assistant. Some proof assistants such as Mizar or Alf do not follow exactly the above scheme: Mizar has a declarative style for proof which is (in theory) readable by a human and checked by a limited checker (This proof style has been adapted to Coq and Isabelle). Unfortunately, there is no formal description of the Mizar proof checker. Alf on the other hand is based on proof theory and requires the user to basically write the complete proof tree just leaving out a few details. The logic is very well formalized and simple, but writing proof is tedious and not similar to the usual practice of informal mathematics.

← Version précédente		Version du 13 janvier 2011 à 11:19
Ligne 211 :		Ligne 211 :
	'''2.a - Core termination criterion''' (delivered 09/2010)		'''2.a - Core termination criterion''' (delivered 09/2010)

	This first test is now part of PML. Since primitive recursive function isn't enough in practice, even for proofs, a subtler and more ~~powerfull~~ termination criterion has been implemented. This is an extension of the "size change principle" of Lee, Jones and Ben-Amram [LJ01]. This test successfully checks termination for primitive recursion, lexicographic ordering and permutation of arguments and thus covers most simple practical cases. The implementation is quite similar to the original size-change principle, but the proof of correctness is surprisingly more difficult: see [Hyv10b].		This first test is now part of PML. Since primitive recursive function isn't enough in practice, even for proofs, a subtler and more powerful termination criterion has been implemented. This is an extension of the "size change principle" of Lee, Jones and Ben-Amram [LJ01]. This test successfully checks termination for primitive recursion, lexicographic ordering and permutation of arguments and thus covers most simple practical cases. The implementation is quite similar to the original size-change principle, but the proof of correctness is surprisingly more difficult: see [Hyv10b].


Ligne 248 :		Ligne 248 :
	'''3.a - A first compiler using LLVM''' (beginning 12/2010, delivered 1/2012) LLVM is a compiler infrastructure providing many tools: compilation strategy, virtual instruction set, compiler infrastructure, tools to write high level virtual machines, etc. LLVM is very attractive, because it is rather simple to use (it even has an OCaml interface) and can compile for a bytecode interpreter, can be used as a JIT compiler or a standard compiler. Moreover, it support a lot of platforms. It also provide some optimizations, which is important. We think that writing a compiler, with no optimization, for PML using LLVM should not be too hard (this is important that this task be easy, because this is not really research ...)		'''3.a - A first compiler using LLVM''' (beginning 12/2010, delivered 1/2012) LLVM is a compiler infrastructure providing many tools: compilation strategy, virtual instruction set, compiler infrastructure, tools to write high level virtual machines, etc. LLVM is very attractive, because it is rather simple to use (it even has an OCaml interface) and can compile for a bytecode interpreter, can be used as a JIT compiler or a standard compiler. Moreover, it support a lot of platforms. It also provide some optimizations, which is important. We think that writing a compiler, with no optimization, for PML using LLVM should not be too hard (this is important that this task be easy, because this is not really research ...)

	A polish phd student Wojciech Matyjewicz has started to work on this in ~~december~~. He visited the LAMA during one week to start the project. It is important to note that he is a first year phd in Poland and the first year there is equivalent to our Master 2. Which means that Wojciech Matyjewicz is a potential candidate.		A polish phd student Wojciech Matyjewicz has started to work on this in December. He visited the LAMA during one week to start the project. It is important to note that he is a first year phd in Poland and the first year there is equivalent to our Master 2. Which means that Wojciech Matyjewicz is a potential candidate.

	Then, we would like to improve our compiler in various direction. We mention here the ones that are innovative in this domain (we should also consider more standard optimization, but we do not mention them specifically).		Then, we would like to improve our compiler in various direction. We mention here the ones that are innovative in this domain (we should also consider more standard optimization, but we do not mention them specifically).

	'''3.b - Representation of cartesian product and disjoint sum''' (beginning 12/2010, delivered 1/2012 for product) PML allows only one kind of cartesian product which in general (because of multiple inheritance and implicit subtyping) must be represented as a table (hash-table or maps based on binary search trees). These can impact performance. We plan to generate extra constraints for each occurrence of a constructor of a cartesian product in a program. Then, solving this constraint in a way that maximize speed (or size) should allow for a representation of cartesian product that is more efficient than using, for instance, OCaml. The same kind of optimization (with a different optimization criterion) should be done for sum types and the implementation of pattern matching. This ~~optimisation~~ should be included in the first compiler because the ~~implentation~~ with tables is too costly for a temporary solution.		'''3.b - Representation of cartesian product and disjoint sum''' (beginning 12/2010, delivered 1/2012 for product) PML allows only one kind of cartesian product which in general (because of multiple inheritance and implicit subtyping) must be represented as a table (hash-table or maps based on binary search trees). These can impact performance. We plan to generate extra constraints for each occurrence of a constructor of a cartesian product in a program. Then, solving this constraint in a way that maximize speed (or size) should allow for a representation of cartesian product that is more efficient than using, for instance, OCaml. The same kind of optimization (with a different optimization criterion) should be done for sum types and the implementation of pattern matching. This optimization should be included in the first compiler because the implantation with tables is too costly for a temporary solution.

	'''3.c - Unboxing''' (depends on some parts of 3.b, beginning 1/2012, delivered 1/2013) In general, 32 bits integer and floating point number are boxed (that is represented by a pointer). This allows a more elegant language. This can lead to major impact on performance especially when arrays are involved. We think that constraint-checking is a good framework to propagate type information and allow efficient unboxing. Nevertheless, doing enough unboxing to try to match the performance of low level languages like C is very hard. We hope that we can reuse some of the work of task 3.b, because unboxing can be seen also as the optimization of the representation of a cartesian product with only one field.		'''3.c - Unboxing''' (depends on some parts of 3.b, beginning 1/2012, delivered 1/2013) In general, 32 bits integer and floating point number are boxed (that is represented by a pointer). This allows a more elegant language. This can lead to major impact on performance especially when arrays are involved. We think that constraint-checking is a good framework to propagate type information and allow efficient unboxing. Nevertheless, doing enough unboxing to try to match the performance of low level languages like C is very hard. We hope that we can reuse some of the work of task 3.b, because unboxing can be seen also as the optimization of the representation of a cartesian product with only one field.
Ligne 258 :		Ligne 258 :
	'''3.d - compilation of affectation (reference and arrays) and IO''' (depend upon 1.c, beginning 09/2012, delivered 03/2014) After adapting uniqueness typing to PML (task 1.c), we will be able to compile affectation and IO imperatively as in any imperative programming language.		'''3.d - compilation of affectation (reference and arrays) and IO''' (depend upon 1.c, beginning 09/2012, delivered 03/2014) After adapting uniqueness typing to PML (task 1.c), we will be able to compile affectation and IO imperatively as in any imperative programming language.

	'''3.e - Garbage collection''' (beginning 01/2014, delivered 09/2014) For simplicity reasons, the first compiler will simply use Boehm's garbage collector. This garbage collector is relatively efficient and simple to use. However, Boehm's GC isn't ~~optimised~~ for the kind of allocations used in a functional language. Moreover, having a multithreaded GC could prove ~~usefull~~ in moder environment. We thus plan to replace Boehm's GC by a dedicated GC tuned for our purposes.		'''3.e - Garbage collection''' (beginning 01/2014, delivered 09/2014) For simplicity reasons, the first compiler will simply use Boehm's garbage collector. This garbage collector is relatively efficient and simple to use. However, Boehm's GC isn't optimized for the kind of allocations used in a functional language. Moreover, having a multithreaded GC could prove useful in moder environment. We thus plan to replace Boehm's GC by a dedicated GC tuned for our purposes.

	Writing a GC that is both efficient and correct is not easy, and this sub-task is rather orthogonal to the PML language, which explains why it only comes later during the project. Nevertheless, we feel it is necessary to go through the trouble if we want to be as efficient (or even better, more efficient) than existing functional languages...		Writing a GC that is both efficient and correct is not easy, and this sub-task is rather orthogonal to the PML language, which explains why it only comes later during the project. Nevertheless, we feel it is necessary to go through the trouble if we want to be as efficient (or even better, more efficient) than existing functional languages...
Ligne 291 :		Ligne 291 :
	The validation requires to write numerous examples to check that we fulfill our main goal, which is that all programs (with or without proof) are written in the best possible way. This work being research, we think that it is important that any piece of code written in PML that does not look ''right'' is carefully examined to check that this is not due to a defect in language design.		The validation requires to write numerous examples to check that we fulfill our main goal, which is that all programs (with or without proof) are written in the best possible way. This work being research, we think that it is important that any piece of code written in PML that does not look ''right'' is carefully examined to check that this is not due to a defect in language design.

	Christophe Mouilleron and Erik Martin-Dorel started to work on the ~~axiomatisation~~ of computer arithmetics within an ongoing PEPS project. This is a good test for PML and moreover a requirement		Christophe Mouilleron and Erik Martin-Dorel started to work on the axiomatization of computer arithmetics within an ongoing PEPS project. This is a good test for PML and moreover a requirement
	because we want PML to be a real programming language and ~~thefore~~ the limited arithmetic of processors (32 and 64 bits integer and floating point number) must be supported by PML. However, proving software using them is not trivial at all and Christophe Mouilleron member of the Arénaire team in ENS Lyon is a specialist in this domain.		because we want PML to be a real programming language and therefore the limited arithmetic of processors (32 and 64 bits integer and floating point number) must be supported by PML. However, proving software using them is not trivial at all and Christophe Mouilleron member of the Arénaire team in ENS Lyon is a specialist in this domain.

	Tom Hirschowitz and Christophe Raffalli already started (and almost finished) a proof in PML that		Tom Hirschowitz and Christophe Raffalli already started (and almost finished) a proof in PML that
Ligne 302 :		Ligne 302 :
	a sufficient corpus to say in which respect we fulfilled our goals.		a sufficient corpus to say in which respect we fulfilled our goals.

	==== Task 6 - ~~Optimisation~~ of PML (transverse task) ====		==== Task 6 - Optimization of PML (transverse task) ====

	Coordinator: C. Raffalli		Coordinator: C. Raffalli
Ligne 308 :		Ligne 308 :
	Participants: All (anyone could optimize the part of PML he was involved in).		Participants: All (anyone could optimize the part of PML he was involved in).

	Some of the choice in the design of PML involve rather complex algorithm. Notably, this is the case of the constraint checking algorithm and completion procedure. The first implementation is not trivial but not optimized either. And very often, we have discoverd and will continue to discover that PML is too slow. This goal of this ~~trasversal~~ task is to ensure that PML is usable.		Some of the choice in the design of PML involve rather complex algorithm. Notably, this is the case of the constraint checking algorithm and completion procedure. The first implementation is not trivial but not optimized either. And very often, we have discoverd and will continue to discover that PML is too slow. This goal of this transversal task is to ensure that PML is usable.

	Currently, some optimisations were already added. For instance, PML uses a sat solver for various		Currently, some optimisations were already added. For instance, PML uses a sat solver for various
	tasks: completeness and usefulness of cases in pattern matching and dealing with negative		tasks: completeness and usefulness of cases in pattern matching and dealing with negative
	hypothesis (like <tt>x</tt> is not equal to <tt>S[x]</tt>) in the completion procedure. Improving the sat solver using J.C. Filliâtre work [] and ~~simploifying~~ the formula before giving them to the sat solver were a major improvement.		hypothesis (like <tt>x</tt> is not equal to <tt>S[x]</tt>) in the completion procedure. Improving the sat solver using J.C. Filliâtre work [] and simplifying the formula before giving them to the sat solver were a major improvement.

	A lot of other optimisations are planned:		A lot of other optimisations are planned:
	* The graph used to encode the typing constraints should probably be reduced (that is we should compute its transitive reduction).		* The graph used to encode the typing constraints should probably be reduced (that is we should compute its transitive reduction).
	* The completion procedure stores a set of terms of the language and we need a fast way to recover the set of all term using a given sub-term. The current implementation is too ~~naïve~~.		* The completion procedure stores a set of terms of the language and we need a fast way to recover the set of all term using a given sub-term. The current implementation is too naive.
	* ...		* ...

ANR PML - Historique des versions

Raffalli : /* Context and positioning of the proposal */

Thirs : /* Context and positioning of the proposal */

Thirs : /* Context and positioning of the proposal */

Raffalli : /* Annexes */

Raffalli : /* Scientific justification of requested budget */

Raffalli : /* Scientific and technical program, project management */

Thirs : /* Tom Hirshowitz (LAMA, Chambéry) */

Raffalli : /* Involvement of project participants to other grants, contracts, etc … */

Raffalli : /* Involvement of project participants to other grants, contracts, etc … */

Raffalli : /* Scientific and technical description */

Raffalli : /* Context and positioning of the proposal */

Thirs : /* Context and positioning of the proposal */

Thirs : /* Context and positioning of the proposal */

Raffalli : /* Annexes */

Raffalli : /* Scientific justification of requested budget */

Raffalli : /* Scientific and technical program, project management */

Thirs : /* Tom Hirshowitz (LAMA, Chambéry) */

Raffalli : /* Involvement of project participants to other grants, contracts, etc … */

Raffalli : /* Involvement of project participants to other grants, contracts, etc … */

Raffalli : /* Scientific and technical description */