Typed Lambda Calculi and Applications

DOI10.1007/B135690zbMATH Open1114.03029OpenAlexW2501230561MaRDI QIDQ5704010FDOQ5704010

Authors: Hugo Herbelin 

Publication date: 11 November 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b135690

Recommendations

• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• A classical sequent calculus with dependent types
• scientific article; zbMATH DE number 823591
• scientific article; zbMATH DE number 1678362
• Denotational semantics of the simplified lambda-mu calculus and a new deduction system of classical type theory

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cited In (7)

• Intuitionistic Letcc via Labelled Deduction
• Adding Negation to Lambda Mu
• Title not available (Why is that?)
• Dualized simple type theory
• Game semantics for dependent types
• A classical sequent calculus with dependent types
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control

This page was built for publication: Typed Lambda Calculi and Applications

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