1 Search Results for "Barendregt, Henk P."


Document
Automata Theoretic Account of Proof Search

Authors: Aleksy Schubert, Wil Dekkers, and Henk P. Barendregt

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)


Abstract
Automata theoretical techniques are developed that handle inhabitant search in the simply typed lambda calculus. The automata-theoretic model for inhabitant search, which can be viewed as proof search by the Curry-Howard isomorphism, is proven to be adequate by reduction of the inhabitant existence problem to the emptiness problem for the automata. To strengthen the claim, it is demonstrated that the latter has the same complexity as the former. We also discuss the basic closure properties of the automata.

Cite as

Aleksy Schubert, Wil Dekkers, and Henk P. Barendregt. Automata Theoretic Account of Proof Search. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 128-143, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{schubert_et_al:LIPIcs.CSL.2015.128,
  author =	{Schubert, Aleksy and Dekkers, Wil and Barendregt, Henk P.},
  title =	{{Automata Theoretic Account of Proof Search}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{128--143},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.128},
  URN =		{urn:nbn:de:0030-drops-54113},
  doi =		{10.4230/LIPIcs.CSL.2015.128},
  annote =	{Keywords: simple types, automata, trees, languages of proofs}
}
  • Refine by Author
  • 1 Barendregt, Henk P.
  • 1 Dekkers, Wil
  • 1 Schubert, Aleksy

  • Refine by Classification

  • Refine by Keyword
  • 1 automata
  • 1 languages of proofs
  • 1 simple types
  • 1 trees

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2015

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail