A. Alvarado-]-amerkad, Y. Bertot, L. Pottier, L. Et-rideau, S. Inria et al., Mathematics and proof presentation in Pcoq Une bibliothèque Coq pour le traitement des langues naturelles Proof automation for type-logical grammars. Rapport technique , Notes pour le cours d'ESSLLI Proof assistants using dependent type systems. Handbook of Automated Reasoning Interactive Theorem Proving and Program Development. Coq'Art : The Calculus of Inductive Constructions Coq team, The Coq proof assistant, reference manual An axiomatization of linear temporal logic in the calculus of inductive constructions Intentional Logic and Logical Grammar, Réflexion pour la réécriture dans le calcul des constructions inductives Proof by Pointing. Symposium on Theoretical Aspects of Computer Software, Japon. [Chomsky, 1957] Chomsky N., Syntactic structures. Mouton & Co. [Coq team Conception de langages pour décrire les preuves et les automatisations dans les outils d'aidè a la preuve La logique. Flammarion. [GAMUT, 1991] GAMUT L., Language and Meaning, pp.801-813, 1994.

J. Girard and L. Logic, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00075966

E. Lyon, Derivations as Proofs, a Logical Approach to Minimalism. [Lescanne, 2004] Lescanne P., Mechanizing epistemic logic with coq

R. Montague, The proper treatment of quantification in ordinary English. Formal Philosophy. Selected Papers of Richard Montague, 1974.

R. Moot and J. Ross, Proof Nets for Linguistic Analysis Constraints on Variables in Syntax, Computational Semantics in Type Theory. Mathématiques et sciences humaines MIT. [Steedman, 1996] Steedman M., Surface Structure and Interpretation, 1967.