The Coq mailing list

[Carlos Olarte <carlos.olarte AT gmail.com>]

Dear Alex,

 We used PHOAS [4] to encode the binders of (first order) linear logic.  The 'forall T' construction is needed to avoid exotic terms (Ie, terms that do not correspond to any syntax) 

Roughly, since the construction is parametric on any Type, an inhabitant of Term or Aprop cannot do pattern matching on the input and generate (structurally) different formulas. 

This link from Adam Chilipala's book is quite useful to understand the technique. 

http://adam.chlipala.net/cpdt/html/Hoas.html

Best 

Carlos 

On Sun, 1 Jul 2018 at 03:03 ikdc <ikdc AT mit.edu> wrote:

Looks like a PHOAS construction; see http://adam.chlipala.net/papers/PhoasICFP08/ for details.

(Reference [4] in the paper you linked.)

On Jun 30, 2018 20:24, Alex Meyer <alex153 AT outlook.lv> wrote:

I am reading about mechanization of linear logic in Coq

http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf and

https://github.com/brunofx86/LL and I have trouble to understand the the function definition Term(and other function definitions involving forall) from

https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v:

Definition Term := forall T:Type,  term T. (* type for terms *)
Definition AProp := forall T:Type, aprop T. (* type for atomic propositions *)

Why we need forall construction in function definition, what additional meaning it gives? Is is creating some kind of set - i.e. - that function returns set of results - one result for each type.

I asked this question on stackoverflow:

https://stackoverflow.com/questions/51017013/what-coq-function-definition-definition-term-forall-t-type-term-t-means

and received one answer there but I would like to get more elaborate answer, I still does not understand this this construction. Maybe there is some good and exact reference in literature?