Realizing the dependently typed -calculus

DOI10.4230/LIPICS.ICLP.2010.294MaRDI QIDQ2883111zbMATH OpenOpenAlexFDO

Authors Zachary Snow

Publication date 11 May 2012

Full work available at URL http://subs.emis.de/LIPIcs/frontdoor_37b5.html

zbMATH Keywords

logical frameworkslogic programming

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Recommendations

• Encoding a dependent-type λ-calculus in a logic programming language
• scientific article; zbMATH DE number 4164201
• scientific article; zbMATH DE number 65533
• A framework for defining logics
• Using typed lambda calculus to implement formal systems on a machine

Cited in

(10)

• scientific article; zbMATH DE number 4164201 (Why is no real title available?)
• scientific article; zbMATH DE number 65533 (Why is no real title available?)
• Implicit typing à la ML for the join-calculus
• Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
• Encoding a dependent-type λ-calculus in a logic programming language
• scientific article; zbMATH DE number 2185726 (Why is no real title available?)
• scientific article; zbMATH DE number 2185664 (Why is no real title available?)
• Some logical and syntactical observations concerning the first-order dependent type system λP
• Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
• Using typed lambda calculus to implement formal systems on a machine

Describes a project that uses

Uses Software

• Abella
• Tac
• Twelf
• Prolog

This page was built for publication: Realizing the dependently typed \(\lambda\)-calculus

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