, Frederic Gilbert Extending higher-order logic with predicate subtyping: application to PVS, 2018.
On irrelevance and algorithmic equality in predicative type theory, 2012. ,
Introduction to generalized type systems, Journal of functional programming, vol.1, issue.2, pp.125-154, 1991. ,
Lambda calculi with types, handbook of logic in computer science vol, vol.ii, 1992. ,
The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997. ,
URL : https://hal.archives-ouvertes.fr/inria-00069968
Type-checking injective pure type systems, Journal of Functional Programming, vol.9, issue.06, pp.675-698, 1999. ,
Towards a mathematical analysis of the coquand-huet calculus of constructions and the other systems in barendregts cube, 1988. ,
An implicit Calculus of Constructions with dependent sums and decidable type inference, 2015. ,
URL : https://hal.archives-ouvertes.fr/tel-01197380
Principles of obj2, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp.52-66, 1985. ,
A short and flexible proof of strong normalization for the calculus of constructions, International Workshop on Types for Proofs and Programs, pp.14-38, 1994. ,
Modular proof of strong normalization for the calculus of constructions, Journal of Functional Programming, vol.1, issue.02, pp.155-189, 1991. ,
Interprétation fonctionelle etéliminationetélimination des coupures de larithmétique dordre supérieur, 1972. ,
Occurrence typing modulo theories, ACM SIGPLAN Notices, vol.51, pp.296-309, 2016. ,
Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, issue.1, pp.279-308, 1993. ,
Hybrid type checking, ACM Transactions on Programming Languages and Systems, vol.32, issue.TOPLAS, p.6, 2010. ,
Ecc, an extended calculus of constructions, Logic in Computer Science, 1989. LICS'89, Proceedings., Fourth Annual Symposium on, pp.386-395, 1989. ,
Pvs: A prototype verification system, International Conference on Automated Deduction, pp.748-752, 1992. ,
The formal semantics of pvs, 1999. ,
Liquid types, ACM SIGPLAN Notices, vol.43, pp.159-169, 2008. ,
Subtypes for specifications: Predicate subtyping in pvs, IEEE Transactions on Software Engineering, vol.24, issue.9, pp.709-720, 1998. ,
Pure type system conversion is always typable, Journal of Functional Programming, vol.22, issue.2, pp.153-180, 2012. ,
URL : https://hal.archives-ouvertes.fr/inria-00497177
Subset coercions in coq, International Workshop on Types for Proofs and Programs, pp.237-252, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00628869
A realizability interpretation of the theory of species, Logic Colloquium, pp.240-251, 1975. ,
Een nadere bewijstheoretische analyse van gstts, 1989. ,
Sterke normaliszatie in c a la tait, Notes of atalk held at the Intercity Seminar on Typed Lambda Calculus, 1989. ,
Strong normalization in type systems: A model theoretical approach, Annals of Pure and Applied Logic, vol.73, issue.1, pp.53-78, 1995. ,
This final step uses in turn termination in order to ensure the success of the expected algorithms. The proof of these three successive steps involves no further specific difficulty. Last, complete algorithms of type-checking and type inference are defined as follows, which states that whenever ? M : T is derivable (resp. ? T : s and ? M : T are derivable), then Infer-type-aux(? | M ) outputs some term successfully (resp. Check-type-aux(? | M | T ) succeeds), vol.4130, pp.604-618, 2006. ,
, Check-wf(? ) is defined as follows: if ? = ?, terminate successfully. Else, ? has the form ? , v : T. If v ? DV (? ) and Check-wf(? ) succeeds, continue as follows: if Infer-type-aux(? | T ) returns s(v) successfully, terminate successfully, all other cases, fail. Infer-type(? | M ) is defined as follows: if Check-wf(? ) succeeds, return Infer-type-aux(? | M ), else fail. Check-type(? | M | T ) is defined as follows: if Check-wf(? ) succeeds, continue as follows. If T = Kind and Infer-type-aux(? | M ) returns Kind, terminate successfully. If T = Kind and Infer-type-aux(? | T ) returns some
, The specifications expected from these algorithms are the following
, Theorem 13. The algorithms Check-wf, Infer-type, and Check-type always terminate, and admit the following properties:-Check-wf(? ) succeeds if and only if ? W F is derivable-Infer-type(? | M ) succeeds if only if there exists a term T such that ? M : T is derivable, in which case it outputs such a term-Check-type(? | M | T ) succeeds if only if ? M : T is derivable