Published: 17th November 2023
DOI: 10.4204/EPTCS.396
ISSN: 2075-2180


Proceedings of the 18th International Workshop on
Logical Frameworks and Meta-Languages: Theory and Practice
Rome, Italy, 2nd July 2023

Edited by: Alberto Ciaffaglione and Carlos Olarte

Invited Paper: On the Practicality and Soundness of Refinement Types
Niki Vazou
Contextual Refinement Types
Antoine Gaulin and Brigitte Pientka
Semi-Automation of Meta-Theoretic Proofs in Beluga
Johanna Schwartzentruber and Brigitte Pientka
Parallel Verification of Natural Deduction Proof Graphs
James T. Oswald and Brandon Rozek
An Interpretation of E-HA^w inside HA^w
Félix Castro


This volume contains a selection of papers presented at LFMTP 2023, the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. The workshop, affiliated with the 8th International Conference on Formal Structures for Computation and Deduction (FSCD), was held in Rome, Italy, on July 2, 2023. We are very grateful to the organization of FSCD for providing the infrastructure and coordination with other events.

Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop brings together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.

For this edition, we received 5 submissions, which were reviewed by at least three members of the program committee. After thorough evaluation, the program committee decided to accept the 5 papers for presentation and selected 4 for inclusion in the present EPTCS volume.

We want to express our sincere thankfulness to all the authors who submitted papers to the workshop. We would also like to acknowledge the exceptional efforts of the program committee, that ensured the high quality of the event. The program committee was formed by Roberto Blanco (MPI-SP), Frédéric Blanqui (Inria), Ana Bove (Chalmers University of Technology), Amy Felty (University of Ottawa), Assia Mahboubi (Inria), Narciso Martí-Oliet (Universidad Complutense de Madrid), Gopalan Nadathur (University of Minnesota), Clément Pit-Claudel (Amazon AWS), Andrei Popescu (University of Sheffield), and Claudio Sacerdoti Coen (University of Bologna). We extend our appreciation to the external reviewers, Théo Winterhalter and Samuele Maschio, for their detailed comments engaging in fruitful discussions.

Lastly, we would like to convey to Niki Vazou our deep gratitude for her invaluable contribution as the invited speaker at LFMTP 2023.

October 04, 2023

Alberto Ciaffaglione and Carlos Olarte.
PC chairs of LFMTP 2023.

On the Practicality and Soundness of Refinement Types

Niki Vazou (IMDEA Software Institute)

Refinement types [5, 3] are a software verification technique that extends types of an existing programming language with logical predicates, to verify critical program properties not expressible by the existing type system. As an example, consider the type of the list indexing function (!!) that takes as input a list xs and an index i and returns the ith element of xs

  Existing Type : (!!) :: [a] -> Int -> a 
   Refined Type : (!!) :: xs:[a] -> i:{Int | 0 <= i < len xs} -> a

Here, the two arguments are named and the logical predicate 0 <= i < len xs is used to refine the type of the index expressing safe indexing. With this refinement type, each time list indexing is used, i.e., xs !! i, the refinement type checker will check that the index i is within bounds.

Refinement Types are Designed to be Practical

Refinement type are naturally integrated in existing programming languages. For example, in Liquid Haskell [13], refinement types are integrated as special Haskell comments that are interpreted by the refinement type checker and ignored by the Haskell compiler. Thus, refinement types provide a formal verification extension to an existing programming language, preserving the runtime semantics, development tools (e.g., editor and cloud integration support), and optimized libraries of the host language.

Verification is automated using SMT solvers [1]. For example, to show that [1,2,3] !! 2 is safe, the refinement type checker will generate the Verification Condition (VC) 0 <= 2 < len [1,2,3] that is valid only when the code satisfies the refinement type specifications (here safe-indexing). Then, the VC is passed to an SMT solver that will prove it valid, thus the code is safe.

Finally, refinement types are carefully designed to ensure decidable verification, which is crucial for both practicality and predictability. To establish decidability, refinement types restrict the language of specifications to a decidable fragment of logic, and design the typing rules, that essentially generate the VCs, so that the logical fragment is preserved. To express more complex concepts, such as quantified properties, verification is type based. For example, [{v:Int | v <= 42}] expresses the type of lists of integers where all elements are smaller than 42, but without the need to quantify over the list elements.

In short, refinement types are designed to be naturally integrated, automated, and decidable, i.e., practical. For that reason, they have already been adopted by various programming languages, e.g., Haskell[12], Ruby [6], Scala [4], and Rust [7]. Yet, in the name of practicality, most refinement type implementations, sacrifice soundness.

Are Refinement Types Sound?

A verifier is not sound when it accepts a program that violates its specification. An unsoundness error can be generated by two different sources: a bug in the implementation of the verifier or a bug in the design of the refinement type system.

The implementation of refinement type checkers is usually large and error prone. A refinement type checker has to trust the compiler of the underlying language to generate an intermediate program representation (IPR), the type checking rules (adapted to accommodate the IPR) to generate logical verification conditions (VC) and the SMT to validate the VCs. All these three trusted components consist of big code bases that inevitably contain bugs and can potentially lead to unsound verification. Indeed, the implementations of F* [10], Stainless [4], and Liquid Haskell [12] respectively consist of 1.3M, 185.3K, and 423K lines of code, and none of these verifiers isolates a trusted kernel. Approximately five unsoundness bugs per year are reported in each system.

The logic of refinement types is not well understood, leaving it unclear for the users what assumptions are safe to be made and which lead to inconsistencies, and thus unsound verification. For example, we recently discovered [11] that function extensionality had been encoded inconsistently in Liquid Haskell for many years. The inconsistent encoding seemed natural and was assumed by both the developers and users of Liquid Haskell. However under the assumption of functional extensionality Liquid Haskell could prove false, invalidating all the user's verification effort.

Having acknowledged the practicality and unsoundness of refinement types, we argue that the community should focus on making refinement types sound, inspired by techniques from the type theory (e.g., Coq [2], Agda [9], and Lean [8]) that design type systems to be sound by construction.


  1. Clark Barrett, Pascal Fontaine & Cesare Tinelli (2017): The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science, The University of Iowa. Available at
  2. Yves Bertot & Pierre Castéran (2004): Coq'Art: The Calculus of Inductive Constructions. Springer. Available at
  3. Tim Freeman & Frank Pfenning (1991): Refinement Types for ML. In: Programming Language Design and Implementation (PLDI), doi:10.1145/113445.113468.
  4. Jad Hamza, Nicolas Voirol & Viktor Kuncak (2019): System FR: Formalized Foundations for the Stainless Verifier. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), doi:10.1145/3360592.
  5. Ranjit Jhala & Niki Vazou (2021): Refinement Types: A Tutorial. Foundations and Trends® in Programming Languages, doi:10.1561/2500000032.
  6. Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster & Emina Torlak (2017): Refinement Types for Ruby. In: Verification, Model Checking, and Abstract Interpretation (VMCAI), doi:10.1007/978-3-319-73721-8_13.
  7. Nico Lehmann, Adam T. Geller, Niki Vazou & Ranjit Jhala (2023): Flux: Liquid Types for Rust. In: Programming Language Design and Implementation (PLDI), doi:10.1145/3591283.
  8. de Moura L., Kong S., Avigad J., van Doorn F. & von Raumer J. (2015): The Lean Theorem Prover. In: International Conference on Automated Deduction (CADE), doi:10.1007/978-3-319-21401-6_26.
  9. Ulf Norell (2009): Dependently Typed Programming in Agda. Springer Berlin Heidelberg, doi:10.1007/978-3-642-04652-0_5.
  10. Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue & Santiago Zanella-Béguelin (2016): Dependent Types and Multi-Monadic Effects in F*. In: Principles of Programming Languages (POPL), doi:10.1145/2837614.2837655.
  11. Niki Vazou & Michael Greenberg (2022): How to Safely Use Extensionality in Liquid Haskell. In: Haskell Symposium, doi:10.1145/3546189.3549919.
  12. Niki Vazou, Eric L. Seidel & Ranjit Jhala (2014): LiquidHaskell: Experience with Refinement Types in the Real World. In: ACM SIGPLAN Symposium on Haskell (Haskell), doi:10.1145/2633357.2633366.
  13. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis & Simon Peyton-Jones (2014): Refinement Types for Haskell. In: International Conference on Functional Programming (ICFP), doi:10.1145/2628136.2628161.