Strong Normalization of a Typed Lambda Calculus for Intuitionistic Bounded Linear-time Temporal Logic

DOI10.4467/20842589RM.12.002.0683zbMATH Open1349.03008OpenAlexW1505662237MaRDI QIDQ5412171

Norihiro Kamide

Publication date: 25 April 2014

Full work available at URL: https://dblp.uni-trier.de/db/journals/rml/rml47.html#Kamide12

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Temporal logic (03B44) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Strong normalizability of typed lambda-calculi for substructural logics

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization 👍 👎
• Strong normalizability of typed lambda-calculi for substructural logics 👍 👎
• Strong normalization from weak normalization in typed \(\lambda\)-calculi 👍 👎
• A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus 👍 👎
• A formalization of strong normalization for simply-typed lambda-calculus and System F 👍 👎
• Computer Science Logic 👍 👎
• Strong normalisation for applied lambda calculi 👍 👎

This page was built for publication: Strong Normalization of a Typed Lambda Calculus for Intuitionistic Bounded Linear-time Temporal Logic

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