We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: A Logic for Reasoning About LF Specifications

Abstract: We present a logic named L_{LF} whose intended use is to formalize properties of specifications developed in the dependently typed lambda calculus LF. The logic is parameterized by the LF signature that constitutes the specification. Atomic formulas correspond to typing derivations relative to this signature. The logic includes a collection of propositional connectives and quantifiers. Quantification ranges over expressions that denote LF terms and LF contexts. Quantifiers of the first variety are qualified by simple types that describe the functional structure associated with the variables they bind; deeper, dependency related properties are expressed by the body of the formula. Context-level quantifiers are qualified by context schemas that identify patterns of declarations out of which actual contexts may be constructed. The semantics of variable-free atomic formulas is articulated via the derivability in LF of the judgements they encode. Propositional constants and connectives are understood in the usual manner and the meaning of quantifiers is explicated through substitutions of expressions that adhere to the type qualifications. The logic is complemented by a proof system that enables reasoning that is sound with respect to the described semantics. The main novelties of the proof system are the provision for case-analysis style reasoning about LF judgements, support for inductive reasoning over the heights of LF derivations and the encoding of LF meta-theorems. The logic is motivated by the paradigmatic example of type assignment in the simply-typed lambda calculus and the proof system is illustrated through the formalization of a proof of type uniqueness for this calculus.
Comments: arXiv admin note: substantial text overlap with arXiv:2105.04110
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Cite as: arXiv:2107.00111 [cs.LO]
  (or arXiv:2107.00111v2 [cs.LO] for this version)

Submission history

From: Gopalan Nadathur [view email]
[v1] Wed, 30 Jun 2021 21:33:24 GMT (93kb)
[v2] Sat, 9 Apr 2022 00:41:42 GMT (93kb)

Link back to: arXiv, form interface, contact.