Logical relations for a logical framework

DOI10.1145/2536740.2536741MaRDI QIDQ2946721zbMATH OpenOpenAlexFDO

Authors Florian Rabe, Kristina Sojakova

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2536740.2536741

zbMATH Keywords

dependent type theoryLFlogical frameworklogical relationmodule systemparametricityTwelf

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Mechanizing metatheory in a logical framework
• scientific article; zbMATH DE number 3902022
• Functional and Logic Programming
• The Twelf Proof Assistant
• Theorem Proving in Higher Order Logics

Cited in

(9)

• Mechanizing proofs with logical relations -- Kripke-style
• Pre-logical relations
• Pointers in Recursion: Exploring the Tropics
• Lax theory morphisms
• Computer Science Logic
• Overcoming Performance Barriers: Efficient Verification Techniques for Logical Frameworks
• Theorem Proving in Higher Order Logics
• LOGICS FOR THE RELATIONAL SYLLOGISTIC
• Systematic translation of formalizations of type theory from intrinsic to extrinsic style

Describes a project that uses

Uses Software

• Twelf

This page was built for publication: Logical relations for a logical framework

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