• Indexed and fibered structures for partial and total correctness assertions 

      Wolter, Uwe Egbert; Martini, Alfio; Haeusler, Edward Hermann (Journal article; Peer reviewed, 2022)
      Hoare Logic has a long tradition in formal verification and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented, and concurrent programs. Here we focus on ...
    • On generalized algebraic theories and categories with families 

      Bezem, Marc; Coquand, Thierry; Dybjer, Peter; Escardo, Martin (Journal article; Peer reviewed, 2021)
      We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define ...