DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2021.6

Church’s Semigroup Is Sq-Universal

Authors: Rick Statman

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract

We prove Church’s lambda calculus semigroup is sq-universal.

Cite as

Rick Statman. Church’s Semigroup Is Sq-Universal. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 6:1-6:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{statman:LIPIcs.FSCD.2021.6,
  author =	{Statman, Rick},
  title =	{{Church’s Semigroup Is Sq-Universal}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{6:1--6:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.6},
  URN =		{urn:nbn:de:0030-drops-142448},
  doi =		{10.4230/LIPIcs.FSCD.2021.6},
  annote =	{Keywords: lambda calculus, Church’s semigroup, sq-universal}
}

Document

DOI: 10.4230/LIPIcs.CSL.2013.634

A New Type Assignment for Strongly Normalizable Terms

Authors: Rick Statman

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract

We consider an operator definable in the intuitionistic theory of monadic predicates and we axiomatize some of its properties in a definitional extension of that monadic logic. The axiomatization lends itself to a natural deduction formulation to which the Curry-Howard isomorphism can be applied. The resulting Church style type system has the property that an untyped term is typable if and only if it is strongly normalizable.

Cite as

Rick Statman. A New Type Assignment for Strongly Normalizable Terms. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 634-652, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{statman:LIPIcs.CSL.2013.634,
  author =	{Statman, Rick},
  title =	{{A New Type Assignment for Strongly Normalizable Terms}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{634--652},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.634},
  URN =		{urn:nbn:de:0030-drops-42233},
  doi =		{10.4230/LIPIcs.CSL.2013.634},
  annote =	{Keywords: lambda calculus}
}

Search Results

Documents authored by Statman, Rick

Church’s Semigroup Is Sq-Universal

Abstract

Cite as

A New Type Assignment for Strongly Normalizable Terms

Abstract

Cite as

Thanks for your feedback!

Could not send message