Higher-order recursion schemes are systems of equations that are used to define finite and infinite labelled trees. Since, as Ong has shown, the trees defined have a decidable monadic second order theory, recursion schemes have drawn the attention of research in program verification, where they sit naturally as a higher-order, functional analogue of Boolean programs. Driven by applications, fragments have been studied, algorithms developed and extensions proposed; the emerging theme is called higher-order model checking. Kobayashi has pioneered an approach to higher-order model checking using intersection types, from which many recent advances have followed. The key is a characterisation of model checking as a problem of intersection type assignment. This dissertation contributes to both the theory and practice of the intersection type approach. A new, fixed-parameter polynomial-time decision procedure is described for the alternating trivial automaton fragment of higher-order model checking. The algorithm uses a novel, type-directed form of abstraction refinement, in which behaviours of the scheme are distinguished according to the intersection types that they inhabit. Furthermore, by using types to reason about acceptance and rejection simultaneously, the algorithm is able to converge on a solution from two sides. An implementation, Preface, and an extensive body of evidence demonstrate empirically that the algorithm scales well to schemes of several thousand rules. A comparison with other tools on benchmarks derived from current practice and the related literature puts it well beyond the state-of-the-art. A generalisation of the intersection type approach is presented in which higher-order model checking is seen as an instance of exact abstract interpretation. Intersection type assignment is used to characterise a general class of safety checking problems, defined independently of any particular representation (such as automata) for a class of recursion schemes built over arbitrary constants. Decidability of any problem in the class is an immediate corollary. Moreover, the work looks beyond whole-program verification, the traditional territory of model checking, by giving a natural treatment of higher-type properties, which are sets of functions.

The logical framework LF and its metalogic Twelf can be used to encode and reason about a wide variety of logics, languages, and other deductive systems in a formal, machine-checkable way. Recent studies have shown that ML-like languages can profitably be extended with a notion of subtyping called refinement types. A refinement type discipline uses an extra layer of term classification above the usual type system to more accurately capture certain properties of terms. I propose that adding refinement types to LF is both useful and practical. To support the claim, I exhibit an extension of LF with refinement types called LFR,work out important details of itsmetatheory, delineate a practical algorithmfor refinement type reconstruction, andpresent several case studies that highlight the utility of refinement types for formalized mathematics. In the end I find that refinement types and LF are a match made in heaven: refinements enable many rich new modes of expression, and the simplicity of LF ensures that they come at a modest cost.

Higher-order recursion schemes are a powerful model of functional computation that grew out of traditional recursive program schemes and generalisations of grammars. It is common to view recursion schemes as generators of possibly-infinite trees, which Ong showed to have a decidable monadic second order theory and opened the door to applications in verification. Kobayashi later presented an intersection type characterisation of the model checking problem, on which most subsequent applied work is based. In recent work, recursion schemes have been considered to play a role similar to Boolean programs in verification of first-order imperative programs: a natural target for abstraction of programs with very large or infinite data domains. In this thesis we focus on the development of model checking algorithms for variants of recursion schemes. We start our contributions with a model checking algorithm inspired by the fully abstract game semantics of recursion schemes, but specified as a goal-directed approach to intersection type inference, that offers a unification of the views of Ong and Kobayashi. We build on this largely theoretical contribution with two orthogonal extensions and practical implementations. First, we develop a new extension of recursion schemes: higher-order recursion schemes with cases, which add non-determinism and a case construct operating over a finite data domain. These additions provide us with a more natural and succinct target for abstraction from functional programs: encoding data using functions inevitably results in an increase in the order and arity of the scheme, which have a direct impact on the worst-case complexity of the problem. We characterise the model checking problem using a novel intersection and union type system and give a practical algorithm for type inference in this system. We have carried out an empirical evaluation of the implementation --- the tool T_RAVMC --- using a variety of problem instances from the literature and a new suite of problem instances derived via an abstraction-refinement procedure from functional programs. Second, we extend our approach from safety properties to all properties expressible in monadic second order logic using alternating parity tree automata as our specification language. We again provide an implementation and an empirical evaluation, which shows that despite the challenges accompanying liveness properties our tool scales beyond the current state of the art.

<p>This thesis studies computational interpretations of the intuitionistic sequent<br />calculus with implicit and explicit structural rules, with focus on the systems<br />with intersection types. The contributions of the thesis are grouped into three<br />parts. In the first part intersection types are introduced into the lambda<br />Gentzen calculus. The second part presents an extension of the lambda<br />Gentzen calculus to a term calculus with resource control, i.e. with explicit<br />operators for contraction and weakening, and apropriate intersection type<br />assignment system which characterises strong normalisation in the proposed<br />calculus. In the third part both previously studied calculi are integrated into<br />one framework by introducing the notion of the resource control cube.</p> / <p>Ова дисертација се бави рачунским интерпретацијама<br />интуиционистичког секвентног рачуна са имплицитним и експлицитним<br />структурним правилима, са фокусом на типске системе са пресеком.<br />Оригинални резултати тезе су груписани у три целине. У првом делу су<br />типови са пресеком уведени у lambda Gentzen рачун. Други део<br />представља проширење lambda Gentzen рачуна на формални рачун са<br />контролом ресурса, тј. са експлицитним операторима контракције и<br />слабљења, као и одговарајући типски систем са пресеком који<br />карактерише јаку нормализацију у уведеном рачуну. У трећем делу оба<br />рачуна су интегрисана у заједнички оквир увођењем структуре resource<br />control cube.</p> / <p>Ova disertacija se bavi računskim interpretacijama<br />intuicionističkog sekventnog računa sa implicitnim i eksplicitnim<br />strukturnim pravilima, sa fokusom na tipske sisteme sa presekom.<br />Originalni rezultati teze su grupisani u tri celine. U prvom delu su<br />tipovi sa presekom uvedeni u lambda Gentzen račun. Drugi deo<br />predstavlja proširenje lambda Gentzen računa na formalni račun sa<br />kontrolom resursa, tj. sa eksplicitnim operatorima kontrakcije i<br />slabljenja, kao i odgovarajući tipski sistem sa presekom koji<br />karakteriše jaku normalizaciju u uvedenom računu. U trećem delu oba<br />računa su integrisana u zajednički okvir uvođenjem strukture resource<br />control cube.</p>

La complexité implicite (ICC) vise à donner des caractérisations de classes de complexité dans des langages de programmation ou des logiques, sans faire référence à des bornes sur les ressources (temps, espace mémoire). Dans cette thèse, nous étudions l’approche de la logique linéaire à la complexité implicite. L’objectif est de donner des caractérisations de classes de complexité, à travers des variantes du lambda-calcul qui sont typables dans de tels systèmes. En particulier, nous considérons à la fois une perspective monovalente et une perspective polyvalente par rapport à l’ICC. Dans le premier cas, le but est de caractériser une hiérarchie de classes de complexité à travers un lambda-calcul élémentaire typé dans la logique linéaire élémentaire (ELL), où la complexité ne dépend que de l’interface d’un programme, c’est à dire son type. La deuxième approche rend compte à la fois des fonctions calculables en temps polynomial et de la normalisation forte, à travers des termes du lambda-calcul pur qui sont typés dans un système inspiré par la logique linéaire Soft (SLL); en particulier, par rapport à l’approche logique ordinaire, ici nous abandonnons la modalité “!” en faveur de l’emploi des types stratifiés, vus comme un raffinement des types intersection non associatifs, afin d’améliorer la typabilité et, en conséquence, l’expressivité. Enfin, nous explorons l’utilisation des types intersection, privés de certaines de leurs propriétés, vers une direction plus quantitative que l’approche qualitative habituelle, afin d’obtenir une borne sur le calcul de lambda-termes purs, en obtenant en plus une caractérisation de la normalisation forte. / In this thesis we explore the linear logic approach to implicit computational complexity, through the design of type assignment systems based on light linear logic, or heavily inspired by them, with the purpose of giving a characterization of one or more complexity classes, through variants of lambda-calculi which are typable in such systems. In particular, we consider both a monovalent and a polyvalent perspective with respect to ICC. In the first one the aim is to characterize a hierarchy of complexity classes through an elementary lambda-calculus typed in Elementary Linear Logic (ELL), where the complexity depends only on the interface of a term, namely its type. The second approach gives an account of both the functions computable in polynomial time and of strong normalization, through terms of pure lambda-calculus which are typed in a system inspired by Soft Linear Logic (SLL); in particular, with respect to the usual logical take, in the latter we give up the “!” modality in favor of employing stratified types as a refinement of non-associative intersection types, in order to improve typability and, as a consequence, expressivity.Finally we explore the use of intersection types, deprived of some of their usual properties, towards a more quantitative approach rather than the usual qualitative one, namely in order to compute a bound on the computation of pure lambda-terms, obtaining in addition a characterization of strong normalization.

L'objet de cette thèse est l'extension des méthodes de la théorie des types intersections non-idempotents, introduite par Gardner et de Carvalho, à des cadres dépassant le lambda-calcul stricto sensu.- Nous proposons d'abord une caractérisation de la normalisation de tête et de la normalisation forte du lambda-mu calcul (déduction naturelle classique) en introduisant des types unions non-idempotents. Comme dans le cas intuitionniste, la non-idempotence nous permet d'extraire du typage des informations quantitatives ainsi que des preuves de terminaison beaucoup plus élémentaires que dans le cas idempotent. Ces résultats nous conduisent à définir une variante à petits pas du lambda-mu-calcul, dans lequel la normalisation forte est aussi caractérisée avec des méthodes quantitatives. - Dans un deuxième temps, nous étendons la caractérisation de la normalisation faible dans le lambda-calcul pur à un lambda-calcul infinitaire étroitement lié aux arbres de Böhm et dû à Klop et al. Ceci donne une réponse positive à une question connue comme le problème de Klop. À cette fin, il est nécessaire d'introduire conjointement un système (système S) de types infinis utilisant une intersection que nous qualifions de séquentielle, et un critère de validité servant à se débarrasser des preuves dégénérées auxquelles les grammaires coinductives de types donnent naissance. Ceci nous permet aussi de donner une solution au problème n°20 de TLCA (caractérisation par les types des permutations héréditaires). Il est à noter que ces deux problèmes n'ont pas de solution dans le cas fini (Tatsuta, 2007).- Enfin, nous étudions le pouvoir expressif des grammaires coinductives de types, en dehors de tout critère de validité. Nous devons encore recourir au système S et nous montrons que tout terme est typable de façon non triviale avec des types infinis et que l'on peut extraire de ces typages des informations sémantiques comme l'ordre (arité) de n'importe quel lambda-terme. Ceci nous amène à introduire une méthode permettant de typer des termes totalement non-productifs, dits termes muets, inspirée de la logique du premier ordre. Ce résultat prouve que, dans l'extension coinductive du modèle relationnel, tout terme a une interprétation non vide. En utilisant une méthode similaire, nous montrons aussi que le système S collapse surjectivement sur l'ensemble des points de ce modèle. / In this dissertation, we extend the methods of non-idempotent intersection type theory, pioneered by Gardner and de Carvalho, to some calculi beyond the lambda-calculus.- We first present a characterization of head and strong normalization in the lambda-mu calculus (classical natural deduction) by introducing non-idempotent union types. As in the intuitionistic case, non-idempotency allows us to extract quantitative information from the typing derivations and we obtain proofs of termination that are far more elementary than those in the idempotent case. These results leads us to define a small-step variant of the lambda-mu calculus, in which strong normalization is also characterized by means of quantitative methods.- In the second part of the dissertation, we extend the characterization of weak normalization in the pure lambda-calculus to an infinitary lambda-calculus narrowly related to Böhm trees, which was introduced by Klop et al. This gives a positive answer to a question known as Klop's problem. In that purpose, it is necessary to simultaneously introduce a system (system S) featuring infinite types and resorting to an intersection operator that we call sequential, and a validity criterion in order to discard unsound proofs that coinductive grammars give rise to. This also allows us to give a solution to TLCA problem #20 (type-theoretic characterization of hereditary permutations). It is to be noted that those two problem do not have a solution in the finite case (Tatsuta, 2007).- Finally, we study the expressive power of coinductive type grammars, without any validity criterion. We must once more resort to system S and we show that every term is typable in a non-trivial way with infinite types and that one can extract semantical information from those typings e.g. the order (arity) of any lambda-term. This leads us to introduce a method that allows typing totally unproductive terms (the so-called mute terms), which is inspired from first order logic. This result establishes that, in the coinductive extension of the relational model, every term has a non-empty interpretation. Using a similar method, we also prove that system S surjectively collapses on the set of points of this model