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

logic programminglogical frameworks

Mathematics Subject Classification ID

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

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

Describes a project that uses

Uses Software

• Prolog
• Abella
• Tac
• Twelf

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)