Typed first-order logic

From the perspectives of both category theory and computer science, it is natural to extend first-order logic with types. Classical many-sorted first-order logic, where types are sorts with no internal structure, is standard. Surprisingly, it’s difficult to find predicate logics including basic algebraic datatypes (product types and sum types). I’m aware of two major threads in the literature, namely

but neither is what I want. I’ve even asked for references on MO.

Logical systems

  • Z specification language (wiki )
    • Based on predicate logic but includes types (free types and product types)
    • Spivey, 1989: An introduction to Z and formal specifications (doi)
    • Woodcock & Davies, 1996: Using Z (pdf)
  • Typed predicate logic (TPL)
    • A meta-language for defining typed logics
    • Turner, 2008: Computable models (doi)
    • Turner, 2009: Computable models (doi)
  • Property theory with Curry typing (PTCT)
    • An unholy combination of first-order logic and typed lambda calculus (with logic)
    • Fox & Lappin, 2004: An expressive first-order logic with flexible typing for natural language semantics (doi, pdf)
    • Fox, 2014: Curry-typed semantics in typed predicate logic (pdf) (PTCT expressed in Turner’s TPL)

Literature

  • Jacobs, 1999: Categorical Logic and Type Theory
    • Sec 2.3: Exponents, products, and coproducts
    • Sec 2.4: Semantics of simple type theory
  • Fiore, Di Cosmo, Balat, 2006: Remarks on isomorphisms in typed lambda calculi with empty and sum types (doi, pdf)
    • Complete proof system for typed lambda calculus with product and sum types
    • Categorical semantics: bicartesian closed categories
  • Gambino & Aczel, 2006: The generalised type-theoretic interpretation of constructive set theory (doi, pdf)
    • “Logic-enriched type theory”: first-order logic with dependent types