Kripke Resource Models of a Dependently-typed, Bunched -calculus

DOI10.1093/logcom/12.6.1061zbMath1017.03005OpenAlexW2118814033MaRDI QIDQ4796463

Samin Ishtiaq, David J. Pym

Publication date: 24 March 2003

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/12.6.1061

zbMATH Keywords

linear logicintuitionistic logictype theorycategorical semanticslogical frameworks\(\lambda \Lambda\)-calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical logic, topoi (03G30) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Combinatory logic and lambda calculus (03B40)

Related Items

Proof-search in type-theoretic languages: An introduction

This page was built for publication: Kripke Resource Models of a Dependently-typed, Bunched  -calculus