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

DOI10.1017/S0956796812000408zbMATH Open1262.68030MaRDI QIDQ4912883

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) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• 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
• A framework for defining logics
• A Linear Spine Calculus
• The view from the left
• Mechanizing metatheory in a logical framework

Related Items (6)

Inductive Beluga: Programming Proofs ⋮ Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis ⋮ Mechanizing proofs with logical relations – Kripke-style ⋮ Harpoon: mechanizing metatheory interactively ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory

Uses Software

• Title not available (Why is that?)

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)