An insider's look at LF type reconstruction: everything you (n)ever wanted to know

DOI10.1017/S0956796812000408MaRDI QIDQ4912883zbMATH OpenFDO

Authors Brigitte Pientka

Publication date 28 March 2013

Published in Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

Beluga languagecontextual modal types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Type Reconstruction for General Refinement Types
• Redundancy elimination for LF
• A Modular Type Reconstruction Algorithm
• scientific article; zbMATH DE number 2182489
• Mechanizing the metatheory of LF

Cites work

• A Linear Spine Calculus
• A framework for defining logics
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Logic, language and computation. Festschrift in Honor of Satoru Takasu
• Mechanizing metatheory in a logical framework
• The view from the left

Cited in

(7)

• Proof-relevant Horn clauses for dependent type inference and term synthesis
• \texttt{slepice}: towards a verified implementation of type theory in type theory
• A case study in programming coinductive proofs: Howe's method
• Inductive beluga: programming proofs
• Type Reconstruction for General Refinement Types
• Mechanizing proofs with logical relations -- Kripke-style
• Harpoon: mechanizing metatheory interactively

Describes a project that uses

Uses Software

• Coq

This page was built for publication: An insider's look at LF type reconstruction: everything you (n)ever wanted to know

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4912883)