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

DOI10.1017/S0956796812000408zbMATH Open1262.68030MaRDI QIDQ4912883FDOQ4912883

Authors: Brigitte Pientka 

Publication date: 28 March 2013

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

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

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)

Cites Work

• 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.
• Mechanizing metatheory in a logical framework
• The view from the left
• Logic, language and computation. Festschrift in Honor of Satoru Takasu
• A Linear Spine Calculus

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

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)