A coinductive approach to proof search through typed lambda-calculi

, &
Annals of Pure and Applied Logic 172 (10):103026 (2021)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2021.103026

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,227

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Strong Normalizability of Typed Lambda-Calculi for Substructural Logics.Motohiko Mouri & Norihiro Kamide - 2008 - Logica Universalis 2 (2):189-207.
Lambda Calculi: A Guide for the Perplexed.Chris Hankin - 1994 - Oxford University Press.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Typed Lambda calculi. S. Abramsky et AL.H. P. Barendregt - 1992 - In S. Abramsky, D. Gabbay & T. Maibaurn (eds.), Handbook of Logic in Computer Science. Oxford University Press. pp. 117--309.
Term-Space Semantics of Typed Lambda Calculus.Ryo Kashima, Naosuke Matsuda & Takao Yuyama - 2020 - Notre Dame Journal of Formal Logic 61 (4):591-600.
Lectures on the Curry-Howard isomorphism.Morten Heine Sørensen - 2007 - Boston: Elsevier. Edited by Paweł Urzyczyn.
Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In M. Baldoni, M. Dastani, B. Liao, Y. Sakurai & R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems. Springer. pp. 202-218.
Linear realizability and full completeness for typed lambda-calculi.Samson Abramsky & Marina Lenisa - 2005 - Annals of Pure and Applied Logic 134 (2-3):122-168.
Compositional Z: Confluence Proofs for Permutative Conversion.Koji Nakazawa & Ken-Etsu Fujita - 2016 - Studia Logica 104 (6):1205-1224.
Weak typed Böhm theorem on IMLL.Satoshi Matsuoka - 2007 - Annals of Pure and Applied Logic 145 (1):37-90.
A Lambda Proof Of The P-w Theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
Remarks on isomorphisms in typed lambda calculi with empty and sum types.Marcelo Fiore, Roberto Di Cosmo & Vincent Balat - 2006 - Annals of Pure and Applied Logic 141 (1):35-50.
Maehara-style modal nested calculi.Roman Kuznets & Lutz Straßburger - 2019 - Archive for Mathematical Logic 58 (3-4):359-385.
Intuitionistic Logic Freed of All Metarules.Giovanna Corsi & Gabriele Tassi - 2007 - Journal of Symbolic Logic 72 (4):1204 - 1218.
On proof terms and embeddings of classical substructural logics.Ken-Etsu Fujita - 1998 - Studia Logica 61 (2):199-221.

Analytics

Added to PP
2021-08-28

Downloads
23 (#685,349)

6 months
5 (#647,370)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Luis Pinto De Sa
Saint Louis University

Citations of this work

No citations found.

Add more citations

References found in this work

Reductive logic and proof-search: proof theory, semantics, and control.David J. Pym & Eike Ritter - 2004 - New York: Oxford University Press. Edited by Eike Ritter.
Counting proofs in propositional logic.René David & Marek Zaionc - 2009 - Archive for Mathematical Logic 48 (2):185-199.

Add more references