The matita interactive theorem prover, 2011. ,
A brief overview of agda -a functional language with dependent types, 2009. ,
Term Rewriting and All That, 1999. ,
Embedding pure type systems in the lambdapi-calculus modulo, TLCA, 2007. ,
A formulation of the simple theory of types, Journal of Symbolic Logic, vol.5, issue.2, pp.56-68, 1940. ,
The rewrite engines competitions : A rectrospective, TACAS, 2019. ,
, Coq development team. The coq proof assistant manual : version 8.9, 2018.
Egison : Non-linear pattern-matching against non-free data types, ArXiv, 2015. ,
Fast matching in combinations of regular equational theories, First International Workshop on Rewriting Logic and its Applications, vol.4, pp.90-109, 1996. ,
Non-linear pattern matching with backtracking for non-free data types, ArXiv, 2018. ,
A framework for defining logics, J. ACM, vol.40, pp.143-184, 1987. ,
The ocaml system release 4.06 : Documentation and user's manual, 1969. ,
Abstract representation of binders in ocaml using the bindlib library, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01972050
Compiling pattern matching to good decision trees, 2008. ,
Term Rewriting, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-00338565
A logic programming language with lambda-abstraction, function variables, and simple unification, Extensions of Logic Programming, 1990. ,
Types and Programming Languages, 2002. ,
Isabelle a generic theorem prover, 1994. ,
CRSX -Combinatory Reduction Systems with Extensions, 22nd International Conference on Rewriting Techniques and Applications (RTA'11), vol.10, pp.81-90, 2011. ,
Mathematical logic as based on the theory of types, American Journal of Mathematics, vol.30, issue.3, pp.222-262, 1908. ,
Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. Theses, Ecole Nationale Supérieure des Mines de Paris, 2015. ,
URL : https://hal.archives-ouvertes.fr/tel-01299180
The twelf proof assistant, TPHOLs, 2009. ,
, There are basic types such as ? bool booleans ? string ? int integers ? float ? unit and type constructor which can be used to build other types, such as list, array, &c. Type constructors are usually used in postfix notation, meaning that the type of a list of integers is noted int list. Such type constructors are said polymorphic, meaning that they can take any type as argument. Arguments of type constructors are usually noted 'a, 'b &c. and read as , &c. We can now mention the essential type constructors
, ? 'a list type of lists. We give some examples of types, (bool * bool) list
, * 'b) list -> 'a -> 'b (** Function searching for a key of type 'a and returning the corresponding element of type
, The infix cons operator :: is of type 'a -> 'a list -> 'a list and puts its left argument on top of its right one. Therefore, A.2.1. Basic values ? Booleans : true and false. ? Integers : 0, 1, ? ? Lists : the empty list