1,721,053 research outputs found
Lincx: a linear logical framework with first-class contexts
Full text linkLinear logic provides an elegant framework for modelling stateful, imperative and con- current systems by viewing a context of assumptions as a set of resources. However, mech- anizing the meta-theory of such systems remains a challenge, as we need to manage and reason about mixed contexts of linear and intuitionistic assumptions. We present Lincx, a contextual linear logical framework with first-class mixed contexts. Lincx allows us to model (linear) abstract syntax trees as syntactic structures that may depend on intuitionistic and linear assumptions. It can also serve as a foundation for reasoning about such structures. Lincx extends the linear logical framework LLF with first-class (linear) contexts and an equational theory of context joins that can otherwise be very tedious and intricate to develop. This work may be also viewed as a generalization of contextual LF that supports both intuitionistic and linear variables, functions, and assumptions. We describe a decidable type-theoretic foundation for Lincx that only characterizes canonical forms and show that our equational theory of context joins is associative and commu- tative. Finally, we outline how Lincx may serve as a practical foundation for mechanizing the meta-theory of stateful systems.La logique linéaire represente une structure élégante pour modeler des systèmes im- pératifs, concurrents et avec des systèmes a états, en représentant un contexte d'hypothèses comme une collection de ressources. Cependant, la mécanisation de la métathéorie de ces systèmes demeure un défi, puisque nous devons gérer et raisonner à propos de contextes d'hypothèses mixtes linéaires et intuitionistiques. Nous présentons Lincx, une structure logique linéaire et contextuelle avec des contextes mixtes de première classe. Lincx nous permet d'établir des modèles (linéaires) d'arbres de syntaxe abstraits en tant que structures syntactiques qui peuvent dependre d'hypothèses intuitionistiques et linéaires. Lincx peut également servir de fondation pour raisonner à propos de telles structures. Lincx étend la structure logique linéaire LLF avec des contextes (linéaires) de premier ordre et une théorie d'equations d'assemblage de contextes qui peut autrement être très fastidieux et complexe à développer. Cet oeuvre peut également être perçu comme une généralisation du LF contextuel qui supporte les fonctions, les hypothéses et les variables intuitionistiques et linéaires. Nous décrivons une fondation de la théorie des types décidable pour Lincx qui ne décrit que les formes canoniques et montrons que notre theorie d'équations d'assemblage de contextes est associative et commutative. Finalement, nous donnons un aperçu de comment Lincx peut servir de fondation pratique pour la mécanisation de la métathéorie de systèmes à états
Well-Founded Recursion over Contextual Objects
Full text linkWe present a core programming language that supports writing well-founded structurally recursive functions using simultaneous pattern matching on contextual LF objects and contexts. The main technical tool is a coverage checking algorithm that also generates valid recursive calls. To establish consistency, we define a call-by-value small-step semantics and prove that every well-typed program terminates using a reducibility semantics. Based on the presented methodology we have implemented a totality checker as part of the programming and proof environment Beluga where it can be used to establish that a total Beluga program corresponds to a proof
A Modal Analysis of Metaprogramming, Revisited (Invited Talk)
No full textMetaprogramming is the art of writing programs that produce or manipulate other programs. This opens the possibility to eliminate boilerplate code and exploit domain-specific knowledge to build high-performance programs. Unfortunately, designing language extensions to support type-safe multi-staged metaprogramming remains very challenging.
In this talk, we outline a modal type-theoretic foundation for multi-staged metaprogramming which supports the generation and the analysis of polymorphic code. It has two main ingredients: first, we exploit contextual modal types to describe open code together with the context in which it is meaningful; second, we model code as a higher-order abstract syntax (HOAS) tree within a context. These two ideas provide the appropriate abstractions for both generating and pattern matching on open code without committing to a concrete representation of variable binding and contexts.
Our work is a first step towards building a general type-theoretic foundation for multi-staged metaprogramming which on the one hand enforces strong type guarantees and on the other hand makes it easy to generate and manipulate code. This will allow us to exploit the full potential of metaprogramming without sacrificing reliability of and trust in the code we are producing and running
Mechanizing Meta-Theory in Beluga (Invited Talk)
No full textMechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga provides a sophisticated infrastructure based on the logical framework LF; in particular, its infrastructure not only supports modelling binders via binders in LF, but extends and generalizes LF with first-class contexts to abstract over a set of assumptions, contextual objects to model derivations that depend on assumptions, and first-class simultaneous substitutions to relate contexts. These extensions allow us to directly support key and common concepts that frequently arise when describing formal systems and derivations within them.
To reason about formal systems, Beluga provides a dependently typed functional language for implementing inductive proofs about derivations as recursive functions on contextual objects following the Curry-Howard isomorphism. Recently, the Beluga system has also been extended with a totality checker which guarantees that recursive programs are well-founded and correspond to inductive proofs and an interactive program development environment to support incremental proof / program construction. Taken together these extensions enable direct and compact mechanizations. To demonstrate Beluga's strength, we develop a weak normalization proof using logical relations. The Beluga system together with examples is available from http://complogic.cs.mcgill.ca/beluga
Indexed reactive programming
No full textLinear Temporal Logic (LTL) is a logic for reasoning about time. It has been used effectively to formally verify systems since it can prove the absence of certain bugs. Under the Curry-Howard correspondence, LTL corresponds to functional reactive programming, a paradigm that handles dataflow propogation. Indexed types, whose Curry-Howard analog is first-order logic, allow types to depend on terms from some index language, and can also ensure program behaviour by virtue of compilation. This thesis introduces Jackrabbit, a reactive programming language with indexed types. We explain the syntax and type system, present a few motivating examples, and prove type safety.La logique temporelle linéaire (LTL) est une logique pour raisonné à propos du temps. Elle est utile pour vérifier les systèmes parce qu’elle est capabale de prouver l’absence de certaines bugs. Sous la correspondence Curry-Howard, l’LTL correspond à la programmation réactive fonctionnelle, une paradigme qui traite la propagation des stream de données. Sous cette même correspondence, les types indexes correpondent à la logique de première ordre, qui permet les types de dépendre sur des termes d’une langage indexe. Les indexes permettent aussi de garantir des propriétés dès compilation. Cette thèse introduit Jackrabbit, une langage réactive avec des types indexes. On explique le syntax et la système de typage, on présente quelques exemples motivants, et on donne une preuve de la sûreté du typage
Tabled higher-order logic programming
No full textdonation from the Siebel Scholars Program. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of the USAF, NSF, the U.S. government or any other entity. Keywords: Logic programming, Type theory, Automated theorem proving, Logi-cal frameworks A logical framework is a general meta-language for specifying and implementing de-ductive systems, given by axioms and inference rules. Based on a higher-order logic programming interpretation, it supports executing logical systems and reasoning with and about them, thereby reducing the effort required for each particular logical system. In this thesis, we describe different techniques to improve the overall performance and the expressive power of higher-order logic programming. First, we introduce tabled higher-order logic programming, a novel execution model where some redundant infor-mation is eliminated using selective memoization. This extends tabled computation to the higher-order setting and forms the basis of the tabled higher-order logic pro
Programming infinite structures using copatterns
No full textInfinite structures are an integral part of computer science as they serve as representations for concepts such as constantly running devices and processes or data communication streams. Due to their importance, it is crucial that programming languages are equipped with adequate means to encode and reason about infinite structures. This thesis investigates the recent idea of copatterns, a device to represent infinite structures in a fashion dual to usual definitions of finite data, by integrating it to Levy's Call-by-Push Value language. We define a coverage algorithm for copattern matching definitions. We prove that evaluation preserves types and that well-typed terms do not get stuck. We define a translation from our language to Levy's and prove that this translation preserves evaluation.Les structures infinies font partie intégrante de l'informatique puisqu'elles permettent la représentation de concepts tels que des processus ou appareils à exécution continue ou de flux de données servant à la communication entre différents appareils. En raison de leur importance, il est crucial que les langages de programmation soient capables d'adéquatement définir les structures infinies. Ce mémoire étudie le concept de comotifs qui permettent de représenter les structures infinies d'une façon duale aux définitions usuelles de données finies. Ce concept est intégré dans une extension du langage d'appel par valeur empilée de Levy. Nous présentons un algorithme de couverture pour les définitions de filtrage par comotif. Nous faisons la démonstration que les séquences d'évaluation préservent les types et que les expressions adéquatement typées ne bloquent pas. Nous présentons aussi une traduction de notre langage vers celui originellement conçu par Levy et nous démontrons que cette traduction s'harmonise avec l'évaluation des deux langages
Implementation of a dependently typed functional programming language
No full textIn recent years, dependent type systems have gathered interest because they make it possible to express stronger properties about programs. However, they are also very verbose. In this thesis, we show how to eliminate some of this verbosity (for the user) by doing reconstruction over dependent types. More precisely, we present the work done in the implementation of the Beluga programming language. Our goal is to present the key issues arising in reconstruction and give a formal and accessible description of ideas that have been around for some time but never given the spotlight. We also prove the soundness of our reconstruction algorithm.Au cours des dernières années, les types dépendants ont reçu un intérêt particulier parce qu'ils permettent d'exprimer des propriétés plus précises sur les programmes. Cependant, ces systèmes de typage sont aussi très redondants. Dans cette thèse, nous allons expliquer comment éliminer une partie de cette redondance en reconstruisant ces types dépendants. Plus précisément, nous présenterons le travail fait sur l'implémentation du langage Beluga. Notre but est de présenter les problématiques importantes liées à la reconstruction de types dépendants et de présenter de façon formelle et accessible certaines idées qui, malgré le fait qu'elle ne sont pas toutes récentes, sont toujours restées dans l'ombre jusqu'à maintenant. Une preuve de correction de notre algorithme de reconstruction est aussi donnée
Proofs and programs about open terms
No full textFormal deductive systems are very common in computer science. They are used to represent logics, programming languages, and security systems. Moreover, writing programs that manipulate them and that reason about them is important and common. Consider proof assistants, language interpreters, compilers and other software that process input described by formal systems. This thesis shows that contextual types can be used to build tools for convenient implementation and reasoning about deductive systems with binders. We discuss three aspects of this: the reconstruction of implicit parameters that makes writing proofs and programs with dependent types easier, the addition of contextual objects to an existing programming language that make implementing formal systems with binders easier, and finally, we explore the idea of embedding the logical framework LF using contextual types in fully dependently typed theory. These are three aspects of the same message: programming using the right abstraction allows us to solve deeper problems with less effort. In this sense we want: easier to write programs and proofs (with implicit parameters), languages that support binders (by embedding a syntactic framework using contextual types), and the power of the logical framework LF with the expressivity of dependent types.Les systèmes critiques comme les systèmes embarqués dans les avions requièrent un niveau de sécurité élevé qui peut seulement être obtenu par des systèmes formels. Les compilateurs certifiés ainsi que les assistants de preuve sont des programmes qui manipulent et qui raisonnent sur ces systèmes. Dans cette thèse, nous utilisons les types contextuels afin de construire de tels outils permettant notamment de raisonner sur des systèmes formels avec lieurs (binders). En particulier, nous abordons les trois points suivants : la reconstruction des paramètres implicites, ce qui simplifie l'écriture des preuves et programmes avec types dépendants ; l'ajout d'objets contextuels à un langage de programmation existant qui facilitent la mise en œuvre des systèmes formels avec des lieurs ; et l'intégration des types contextuels avec des types dépendants au-dessus du cadre logique (logical frameworks) LF. Ces trois facettes reflètent le message suivant : le choix d'une abstraction adéquate nous permet de construire des outils capables de résoudre des problèmes plus complexes plus facilement. Ceci se traduit par la construction de langages de programmation utilisant des paramètres implicites, supportant des lieurs (en intégrant un cadre syntaxique utilisant des types contextuels), et qui utilisent la puissance du cadre logique LF jointe à une théorie des types a la Martin-Löf
Focused inverse method for LF
No full textLogical frameworks allow us to specify formal systems and prove properties about them. One interesting logical framework is Twelf, a language that uses higher order abstract syntax to encode object languages into the meta language. Currently, uniform proofs have been used for describing proof search in backwards logic programming style. However, there are certain limitations to a backward system, for example, loop-detection mechanisms are required for some of the simplest problems to yield a solution. As a consequence, the search for a more effective proof search algorithm prevails and a forward system is proposed. This thesis will discuss the theoretical foundations for a forward uniform sequent calculus and the implementation of an inverse method prover for Twelf.Les cadres logiques nous permettent de spécifier des systèmes formels et de prouver des propriétés à leur sujet. Un cadre logique intéressant est Twelf, un langage qui emploie la syntaxe abstraite d'ordre supérieur pour encoder des langages objet dans le méta-langage. Actuellement, nous employons des preuves uniformes pour décrire la recherche dans le style de programmation logique arrière. Cependant, il y a certaines limitations à un système arrière: des mécanismes de détection de boucle sont nécessaires pour trouver une solution à certains des problèmes les plus simples. Par conséquent, la recherche d'un algorithme plus efficace de recherche de preuve règne et un système vers l'avant est proposé. Cette thèse discutera les bases théoriques d'un calcul séquent uniforme vers l'avant et l'implantation d'un prouveur à méthode inverse pour Twelf
- …
