ABSTRACT. We revisit our formalization of the metatheory of Proto-Quipper in the Hybrid logical framework.  Proto-Quipper contains the core of Quipper, which is a programming language designed to express quantum circuits and allow them to be treated as data.  Hybrid is a system that is designed to support the use of higher-order abstract syntax (also called lambda-tree syntax) for representing and reasoning about formal systems, implemented in the Coq Proof Assistant.  Hybrid follows a two-level approach, where a specification logic (SL) is defined as an inductive type in Coq, and reasoning about an object logic (OL) such as Proto-Quipper is carried out using the SL.  In this work, we adopt a linear SL, which provides infrastructure for reasoning directly about the linear type system of Proto-Quipper.In two-level systems, statements of theorems often relate two or more OL judgments, and a "context relation" is often needed to specify the constraints between them.  In this work, we carry out a more careful study of context relations in a linear setting.  Other goals of revisiting our formalization include: extending the use of higher-order syntax to encode the notion of bound variables in circuits, and improving the representation of subtyping so that it is closer to the original formulation of Proto-Quipper.  The latter allowed us to find an error in one of the on-paper proofs.

ABSTRACT. We use the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative bias, LJF proofs encode term structures as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given the positive bias, LJF proofs yield a structure in which explicit sharing of term structures is possible. In this situation, cut elimination yields a different notion of substitution. We illustrate these two approaches to term representation by applying them to the encoding of untyped λ-terms.

More details can be found at http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lfmtp22-positive-perspective.pdf.

ABSTRACT. Dedukti is a type-checker for the lambda-pi calculus modulo theory, a logical framework that allows the extension of conversion with user-defined rewrite rules. In this paper, we present the implementation of a version of Dowek-Miquel’s intuitionistic set theory in Dedukti. To do so, we adapt this theory - based on the concept of pointed graphs - from Deduction modulo theory to lambda-pi calculus modulo theory, and we formally write the proofs in Dedukti. In particular, this implementation requires the definition of a deep embedding of a certain class of formulas, as well as its interpretation in the theory.

More details can be found at https://hal.archives-ouvertes.fr/hal-03740004.

ABSTRACT. Metaprogramming 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. While this widely used concept is almost as old as programming itself, it has been surprisingly challenging to extend to logical frameworks and type-theoretic proof assistants.

In this talk, we present MINTS, a modal intuitionistic type theory which supports dependently typed  multi-staged programming in the spirit of Scheme or Racket's quote-unquote style. As MINTS is dependently typed, we can not only specify, generate and share code across multiple stages, but also reason about multi-staged programs and prove them correct in MINTS. Theoretically, MINTS extends the Kripke-style modal lambda-calculus by Pfenning and Davies which serves as a logical foundation for simply-typed multi-staged programming to a full Martin-Loef type  theory with a cumulative hierarchy of universes. 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. In addition, it provides a fresh perspective towards internalizing macros or tactics in proof assistants based on type theories.

This is joint work with Jason Z. Hu and Junyoung Jang.

ABSTRACT. Lambek's two calculi, the associative one and the non-associative one, have their advantages and disadvantages for the analysis of natural language syntax by means of categorial grammar. In some cases, associativity leads to over-generation, i.e., validation of grammatically incorrect sentences. In other situations, associativity is useful. We will discuss two approaches. One approach, developed by Morrill and Moortgat, begins with the associative calculus and reconstructs local non-associativity by means of the so-called bracket modalities, ultimately leading to Morrill's CatLog parser. Bracket modalities interact in a subtle way with the subexponential modalities originating in linear logic. Another approach, developed by Moot and Retoré, begins with the non-associative calculus and utilizes multi-modalities, ultimately leading to the Grail parser. We enhance the latter approach in our IJCAR 2022 paper, showing that local associativity may be expressed by means of subexponentials. Some aspects of the two approaches touch Frank Pfenning's work on ordered logic and on adjoint logic. We discuss decidability and undecidability results in both approaches.

ABSTRACT. The dependently typed lambda calculus LF provides a convenient means for encoding specifications of object systems; dependent types in this calculus constitute a natural representation of rule-based relational specifications and lambda terms provide for a higher-order abstract syntax based treatment of binding structure. An important consideration from the perspective of formalizing object systems in this context is how reasoning about such specifications can be supported. One approach towards addressing this issue, pioneered by Frank Pfenning and Carsten Schuermann, is to use LF types with specified modes to represent properties of LF specifications; the validity of these properties is then demonstrated by describing inhabitants for such types and showing their totality relative to the chosen modes. We will describe a different approach in this talk. This approach is based on describing a logic that uses LF typing judgements as atomic formulas and that allows more complex formulas to be constructed using logical connectives and quantification over contexts and term variables. The validity of quantifier-free formulas in the logic is determined by LF derivability and a classical interpretation of the connectives, and quantifiers are interpreted by a substitution semantics. Mechanization of reasoning is realized by describing proof rules that are sound with respect to the semantics. We will discuss a collection of proof rules that encode LF meta-theorems and provide for case analysis and induction based reasoning over LF derivations, in addition to reasoning based on the usual interpretation of logical symbols. This approach shares some aspects with the one explored by Mary Southern and Kaustuv Chaudhuri using the Abella system but differs from it in that LF derivability is treated explicitly in the logic rather than indirectly via a translation to a predicate logic form. The talk will also touch upon the Adelfa proof assistant that implements the logic.

[The talk will be based on collaborative work with Mary Southern andChase Johnson.]

ABSTRACT. A common interest in logical frameworks formed the basis for many years of fruitful and enjoyable collaboration with Frank and his students, both directly and indirectly.  Frank’s development of the Twelf system was instrumental in enabling the use of LF for specifying a wide range of formalisms, ranging from “pure logics” to “practical programming languages.”  Most importantly, the Twelf totality checker for proving All-Exists statements allowed for a human-readable and easily developed proof of type safety for the Standard ML language that not only verified what we already knew, but also fostered the development of a new language definition methodology well-suited to the demands of working at scale.

ABSTRACT. I will discuss some personal perspectives on the "Type Refinement" project initiated by Frank several decades ago, and how it has influenced my research over the years since my PhD.

ABSTRACT. In the design of tools, languages, and frameworks, Frank has been a consistent advocate for a particular flavor of aesthetic minimalism. A valuable trait of minimalist frameworks and tiny programming languages is that they facilitate implementation and reimplementation in multiple contexts with various interfaces. This principle has guided our (Chris and Rob’s) work at and beyond Carnegie Mellon, including for some recent projects we've pursued together. We'll talk about some of our Frank-adjacent projects we've reimplemented on the web, how language minimalism contributed to their success, lessons learned, and a path forward for extending the reach and application of logical frameworks.