Submission by Jevgenijs Sallinens

From POPLmark

[edit] Direct solution for parts 1a, 2a

• Author: Jevgenijs Sallinens.
• Part(s) addressed: 1a, 2a.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: Direct (absolutely concrete, constructive, FOAS).
• Updated 29th July 2007.

Here is presented completely formalized solution for parts 1a and 2a of the POPLmark challenge. Proofs are verified with the proof assistant Coq, version 8.1. Solution directly and adequately represents subtyping relation given in the challenge description. It is consistent in the sense, that relays only on Coq assumptions about inductive definitions, considered to be consistent. In particular, it follows also that no contradiction could be derived from informal assumptions made in the paper proof. Solution is using Coq constructive logic without assumption of excluded middle and is based on arbitrary set of names, equipped with arbitrary decidable equality relation. Here is introduced novel technique based on flat induction principles, used novel notions of alpha-equivalence and substitution relations and demonstrated the usage of strong forms of inductive definitions for relations in conjunction with special supporting and invariance principles.

Here is zipped version for all files:[1]. Files related to this solution: [2] [3] [4] [5] [6] [7] with more details could be found in http://www.mathcoq.com/poplmark.htm.

[edit] Solution with nameless representation for parts 1a and 2a

• Author: Jevgenijs Sallinens.
• Part(s) addressed: 1a, 2a.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: nameless (DeBruijn indices).
• Updated 6th March 2007.

New version of the nameless solution is presented as continuation of the direct solution above. To perform proofs on structure of types, there is introduced special equality relation on types, representing similarity of structures. Induction on structure of types is interpreted as usual induction on types modulo structural equality. As the major result for part2a, there is given explicit operator to perform reduction step for the third subtask of the third part, with direct proof that typing is preserved with this reduction. Some new results (inversions of typing rules) are presented to simplify proofs for arbitrary (possible non-empty) environments. So, the part 3 is resolved in the sense, that there are presented programs to perform reduction and these programs are verified to be compatible with subtyping and typing relations. Also others decidable relations, such as well-formedness conditions, are given in the form of computable operators to the type of booleans, so providing verified basis for programming of all related aspects (except connected with computations for undecidable subtyping and typing relations). There are established relations with name-carrying (absolutely concrete) representation and main results are translated into this representation. In particular, there are given name-carrying forms of preservation and progress theorems.

Related files: [8] [9] [10] [11] [12] [13] [14] with more details could be found in http://www.mathcoq.com/poplmark2.htm.