Auswahl der wissenschaftlichen Literatur zum Thema „Lambda-Pi calculus“

Dependently-typed programming languages are gaining importance, because they can guarantee a wide range of properties at compile time. Their use in practice is often hampered because programmers have to provide very precise types. Gradual typing is a means to vary the level of typing precision between program fragments and to transition smoothly towards more precisely typed programs. The combination of gradual typing and dependent types seems promising to promote the widespread use of dependent types. We investigate a gradual version of a minimalist value-dependent lambda calculus. Compile-time calculations and thus dependencies are restricted to labels, drawn from a generic enumeration type. The calculus supports the usual Pi and Sigma types as well as singleton types and subtyping. It is sufficiently powerful to provide flexible encodings of variant and record types with first-class labels. We provide type checking algorithms for the underlying label-dependent lambda calculus and its gradual extension. The gradual type checker drives the translation into a cast calculus, which extends the original language. The cast calculus comes with several innovations: refined typing for casts in the presence of singletons, type reduction in casts, and fully dependent Sigma types. Besides standard metatheoretical results, we establish the gradual guarantee for the gradual language.

Abstract We characterize the Archimedean vector lattices that admit a positively homogeneous continuous function calculus by showing that the following two conditions are equivalent for each $n$-tuple $\boldsymbol{x} = (x_1,\ldots ,x_n)\in X^n$, where $X$ is an Archimedean vector lattice and $n\in{\mathbb{N}}$: • there is a vector lattice homomorphism $\Phi _{\boldsymbol{x}}\colon H_n\to X$ such that $$\begin{equation*}\Phi_{\boldsymbol{x}}(\pi_i^{(n)}) = x_i\qquad (i\in\{1,\ldots,n\}),\end{equation*}$$where $H_n$ denotes the vector lattice of positively homogeneous, continuous, real-valued functions defined on ${\mathbb{R}}^n$ and $\pi _i^{(n)}\colon{\mathbb{R}}^n\to{\mathbb{R}}$ is the $i^{\text{}}$th coordinate projection;• there is a positive element $e\in X$ such that $e\geqslant \lvert x_1\rvert \vee \cdots \vee \lvert x_n\rvert$ and the norm$$\begin{equation*}\lVert x\rVert_e = \inf\bigl\{ \lambda\in[0,\infty)\:\colon\:\lvert x\rvert{\leqslant}\lambda e\bigr\},\end{equation*}$$defined for each $x$ in the order ideal $I_e$ of $X$ generated by $e$, is complete when restricted to the closed sublattice of $I_e$ generated by $x_1,\ldots ,x_n$. Moreover, we show that a vector space which admits a ‘sufficiently strong’ $H_n$-function calculus for each $n\in{\mathbb{N}}$ is automatically a vector lattice, and we explore the situation in the non-Archimedean case by showing that some non-Archimedean vector lattices admit a positively homogeneous continuous function calculus, while others do not.

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as lambda-bar-mu-calculus, pi-calculus, Positive GSOS specifications, differential lambda-calculus, and the big-step, simply-typed, call-by-value lambda-calculus. Moreover, we design a suitable notion of signature for transition monads.

We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider spi, a pi-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of lambdafail into spi and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in lambdafail via typed processes in spi. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.

The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.

Some alternative characterizations of late full congruences, either strong or weak, are presented. Those congruences are classically defined by requiring the corresponding ground bisimilarity under all name substitutions. <br />We first improve on those infinitary definitions by showing that congruences can be alternatively characterized in the pi-calculus by sticking to a finite<br />number of carefully identified substitutions, and hence, by resorting to only a finite number of ground bisimilarity checks.<br />Then we investigate the same issue in both the ground and the non-ground pi-xsi-calculus, a CCS-like process algebra whose ground version has already been proved to coincide with ground pi-calculus. The pi-xsi-calculus perspective allows processes to be explicitly interpreted as functions of their free names. As a<br />result, a couple of alternative characterizations of pi-congruences are given, each of them in terms of the bisimilarity of one single pair of pi-xsi-processes. In one case, we exploit lambda-closures of processes, so inducing the effective generation<br />of the substitutions necessary to infer non-ground equivalence. In the other case, a more promising call-by-need discipline for the generation of the wanted substitutions is used. This last strategy is also adopted to show a coincidence result with open semantics. <br />By minor changes, all of the above characterizations for late semantics can be suited for congruences of the early family.

The lambda-Pi-calculus modulo theory is a logical framework in which many type systems can be expressed as theories. We present such a theory, the theory U, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of U corresponding to each of these systems, and prove that, when a proof in U uses only symbols of a sub-theory, then it is a proof in that sub-theory.

<p>The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state<br />in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between<br />names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus<br />has connections to local declarations in general; to the mobile processes of the pi-calculus; and to security protocols in the spi-calculus. <br /> This paper introduces a logic of equations and relations which allows one to<br />reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of<br />contextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power but<br />in a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.</p><p>This supersedes the earlier BRICS Report RS-96-31. It also expands on the paper presented in Typed Lambda Calculi and Applications: Proceedings of the Third<br />International Conference TLCA '97, Lecture Notes in Computer Science 1210, Springer-Verlag 1997.</p>

The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus has connections to other kinds of local declaration, and to the mobile processes of the pi-calculus.<br /> <br />This paper introduces a logic of equations and relations which allows one to reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of contextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power but in a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.<br /><br />See the revised version BRICS-RS-97-39.

Le typage permet d'apporter de la sûreté dans la programmation, et il est utilisé au coeur de la majorité des systèmes de preuve. Plus un système de types est expressif, plus il est aisé d'y encoder des invariantsqui seront vérifiés mécaniquement lors du typage. Les types dépendants sont une extension des types simples dans laquelle les types peuvent dépendre de valeurs. Ils permettent par exemple de définir les vecteurs paramétrés par leur longueur. Le sous-typage par prédicat est une autre extension des types simples, dans laquelle les types peuvent être définis par des prédicats. Un sous-type défini par un prédicat, généralement noté { x : A | P(x) }, est habité par les éléments t de type A pour lesquels P(t) est vrai. Cette extension fournit un système de type très riche et intuitif, mais qui rend le typage indécidable.Cet ouvrage est dédié à l'encodage du sous-typage par prédicats dans Dedukti, un cadre logique avec des règles de calcul. On commence par encoder une version explicite du sous-typage par prédicats pour lequel un habitant de { x: A | P(x) } est syntaxiquement différent d'un habitant de A. On montre que tout jugement dérivable dans cette version du sous-typage par prédicat peut être encodé en un jugement dérivable du cadre logique.Le sous-typage par prédicat est souvent utilisé de manière implicite, sans différence syntaxique entre les habitants de A et les habitants de { x: A | P(x) }. On enrichit le cadre logique avec un système de raffinement des termes qui pourra ajouter ces marqueurs syntaxiques. Ce raffineur peut traduire des jugements typables avec du sous-typage par prédicat implicite en des jugements typable avec du sous-typage explicite.L'assistant à la preuve pvs utilise abondamment le sous-typage par prédicat. On montre comment sa bibliothèque standard peut être exportée vers Dedukti. Par ailleurs, PVS ne préserve que des traces de preuves. Dans la pénultième section, on décrit une procédure pour générer des preuves complètes à partir des traces laissées par PVS.La dernière section détaille une architecture pour l'entrepôt et l'échange de preuves formelles, afin de promouvoir l'interopérabilité<br>Safe programming as well as most proof systems rely on typing. The more a type system is expressive, the more these types can be used to encode invariants which are therefore verified mechanically through type checking procedures. Dependent types extend simple types by allowing types to depend on values. For instance, it allows to define the types of lists of a certain length. Predicate subtyping is another extension of simple type theory in which types can be defined by predicates. A predicate subtype, usually noted {x: A | P(x)}, is inhabited by elements t of type A for which P(t) is true. This extension provides an extremely rich and intuitive type system, which is at the heart of the proof assistant PVS, at the cost of making type checking undecidable.This work is dedicated to the encoding of predicate subtyping in Dedukti: a logical framework with computation rules. We begin with the encoding of explicit predicate subtyping for which the terms in {x: A | P(x)} and terms of Aare syntactically different. We show that any derivable judgement of predicate subtyping can be encoded into a derivable judgement of the logical framework. Predicate subtyping, is often used implicitly: with no syntactic difference between terms of type A and terms of type {x: A | P(x) }. We enrich our logical framework with a term refiner which can add these syntactic markers. This refiner can be used to refine judgements typed with implicit predicate subtyping into explicited judgements.The proof assistant PVS uses extensively predicate subtyping. We show how its standard library can be exported to Dedukti. Because PVS only store proof traces rather than complete proof terms, we sketch in the penultimate section a procedure to generate complete proof terms from these proof traces.The last section provides the architecture of a repository dedicated to the exchange of formal proofs. The goal of such a repository is to categorise and store proofs encoded in Dedukti to promote interoperability

Le pi-calcul est une algebre de processus definie a partir de deux concepts : nommer et communiquer. Les noms sont des canaux de communication, et communiquer consiste a echanger des noms. Le pi-calcul permet ainsi de representer des systemes concurrents dont les liens de communication peuvent evoluer dynamiquement. Le pi-calcul possede une grande puissance d'expression. On peut y coder diverses structures de donnees. Il permet de retrouver toute la puissance d'expression du lambda-calcul vu qu'on peut y coder ce dernier. On peut aussi y representer des objets et des objets concurrents ainsi que des calculs d'ordre superieur ou un processus peut etre transmis sur un canal. En utilisant comme seul mecanisme d'evaluation la communication, un langage noyau a ete bati directement sur le pi-calcul. Le pi-calcul a aussi servi de base pour definir de nouveaux calculs. Dans ce travail, nous nous interessons au sous-typage dans le pi-calcul. D'une part, nous definissons un systeme de types pi-sub, qui permet de specifier l'arite d'un canal et son mode d'utilisation : emettre uniquement, recevoir uniquement, emettre et recevoir ou est juste emis ou recu mais jamais utilise pour emettre ou recevoir. Nous proposons un algorithme d'inference de types pour ce systeme de types. Cet algorithme permet alors de detecter des erreurs de communication et de donner une analyse fine de l'utilisation des canaux. D'autre part, la possibilite de coder le lambda-calcul dans le pi-calcul, montre que ce dernier peut servir pour l'etude de la semantique de langages fonctionnels concurrents. Quand nous nous interessons aux langages types, etudier la correspondance entre le typage dans les deux calculs devient une question pertinente. Cela permet aussi de voir si des techniques developpees pour l'un peuvent etre utilisees pour l'autre. Nous etudions ce probleme en presence de sous-typage simple. Pour divers codages du lambda-calcul dans le pi-calcul, nous etudions la correspondance entre le typage dans lambda-sub et le typage dans pi-sub.

La vérification automatique de preuves consiste à faire vérifier par un ordinateur la validité de démonstrations d'énoncés mathématiques. Cette vérification étant purement calculatoire, elle offre un haut degré de confiance. Elle est donc particulièrement utile pour vérifier qu'un logiciel critique, c'est-à-dire dont le bon fonctionnement a un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens, correspond exactement à sa spécification. DEDUKTI est l'un de ces vérificateurs de preuves. Il implémente un système de type, le lambda-Pi-Calcul Modulo, qui est une extension du lambda-calcul avec types dépendants avec des règles de réécriture du premier ordre. Suivant la correspondance de Curry-Howard, DEDUKTI implémente à la fois un puissant langage de programmation et un système logique très expressif. Par ailleurs, ce langage est particulièrement bien adapté à l'encodage d'autres systèmes logiques. On peut, par exemple, importer dans DEDUKTI des théorèmes prouvés en utilisant d'autres outils tels que COQ, HOL ou encore ZENON, ouvrant ainsi la voie à l'interopérabilité entre tous ces systèmes. Le lambda-Pi-Calcul Modulo est un langage très expressif. En contrepartie, certaines propriétés fondamentales du système, telles que l'unicité des types ou la stabilité du typage par réduction, ne sont pas garanties dans le cas général et dépendent des règles de réécriture considérées. Or ces propriétés sont nécessaires pour garantir la cohérence des systèmes de preuve utilisés, mais aussi pour prouver la correction et la complétude des algorithmes de vérification de types implémentés par DEDUKTI. Malheureusement, ces propriétés sont indécidables. Dans cette thèse, nous avons donc cherché à concevoir des critères garantissant la stabilité du typage par réduction et l'unicité des types et qui soient décidables, de manière à pouvoir être implémentés par DEDUKTI. Pour cela, nous donnons une nouvelle définition du lambda-Pi-Calcul Modulo qui rend compte de l'aspect itératif de l'ajout des règles de réécriture dans le système en les explicitant dans le contexte. Une étude détaillée de ce nouveau calcul permet de comprendre qu'on peut ramener le problème de la stabilité du typage par réduction et de l'unicité des types à deux propriétés plus simples, qui sont la compatibilité du produit et le bon typage des règles de réécriture. Nous étudions donc ces deux propriétés séparément et en donnons des conditions suffisantes effectives. Ces idées ont été implémentées dans DEDUKTI, permettant d'augmenter grandement sa généralité et sa fiabilité<br>Automatic proof checking is about using a computer to check the validity of proofs of mathematical statements. Since this verification is purely computational, it offers a high degree of confidence. Therefore, it is particularly useful for checking that a critical software, i.e., a software that when malfunctioning may result in death or serious injury to people, loss or severe damage to equipment or environmental harm, corresponds to its specification. DEDUKTI is such a proof checker. It implements a type system, the lambda-Pi-Calculus Modulo, that is an extension of the dependently-typed lambda-calculus with first-order rewrite rules. Through the Curry-Howard correspondence, DEDUKTI implements both a powerful programming language and an expressive logical system. Furthermore, this language is particularly well suited for encoding other proof systems. For instance, we can import in DEDUKTI theorems proved using other tools such as COQ, HOL or ZENON, a first step towards creating interoperability between these systems.The lambda-Pi-Calculus Modulo is a very expressive language. On the other hand, some fundamental properties such as subject reduction (i.e., the stability of typing by reduction) and uniqueness of types are not guaranteed in general and depend on the rewrite rules considered. Yet, these properties are necessary for guaranteeing the coherence of the proof system, but also for provingthe soundness and completeness of the type-checking algorithms implemented in DEDUKTI. Unfortunately, these properties are undecidable. In this thesis, we design new criteria for subject reduction and uniqueness of types that are decidable in order to be implemented in DEDUKTI.For this purpose, we give a new definition of the lambda-Pi-Calculus Modulo that takes into account the iterative aspect of the addition of rewrite rules in the typing context. A detailed study of this new system shows that the problems of subject reduction and uniqueness of types can be reduced to two simpler properties that we call product compatibility and well-typedness of rewrite rules.Hence, we study these two properties separately and give effective sufficient conditions for them to hold.These ideas have been implemented in DEDUKTI, increasing its generality and reliability

Cette thèse se consacre à l'application de techniques de réalisabilité dans le cadre de l'étude du sens calculatoire de la logique. Dans une première partie, nous rappelons le formalisme de la réalisabilité classique de Krivine, dans lequel nous menons ensuite une étude du contenu opérationnel de tautologies purement classiques. Cette exploration du sens calculatoire de la disjonction classique révèle des comportements riches, avec une forte intuition interactive, qui s'interprètent avantageusement comme des structures de contrôle typées. Afin de mieux comprendre la nature de ces mécanismes, nous définissons ensuite une technique de réalisabilité à la Krivine pour un modèle de calcul concurrent, dans le but d'obtenir une notion de constructivité qui ne soit plus fondée sur l'idée de fonction, mais sur celle de processus interactif. Le cadre ainsi obtenu donne une interprétation réellement concurrente de la logique linéaire dans un calcul de processus dérivé du pi-calcul, permettant d'appliquer au cas concurrent la méthode de spécification précédemment étudiée dans le cas séquentiel. Par la suite, l'étude des traductions de la logique classique vers la logique linéaire mène à reconstruire systématiquement des décompositions interactives du calcul fonctionnel, permettant ainsi de faire le lien au niveau logique entre les réalisabilités classique et concurrente. Dans une dernière partie, nous étudions plus en détail le mode de calcul issu des algèbres de processus, afin de comprendre son système d'ordonnancement. Cette étude mène à la définition d'un modèle de calcul plus géométrique qui permet une exploration formelle de la notion de causalité dans les calculs concurrents.

La logique linéaire fait désormais partie des outils standards en théorie de la démonstration et, de manière plus générale, dans l'étude de la correspondance de Curry-Howard. Nous présentons ici trois directions importantes d'application de méthodes issues de la logique linéaire : - la théorie de la démonstration de la logique classique et ses aspects calculatoires via notamment la sémantique des jeux ; - la complexité implicite à travers les modèles dénotationnels des logiques linéaires à complexité bornée ; - la théorie de la concurrence et ses fondements logiques grâce aux ingrédients apportés par la logique linéaire différentielle. Les approches linéaires offrent ainsi un cadre commun pour l'étude de différents aspects logiques du calcul.