1 Search Results for "Gérard, Ulysse"

Separating Functional Computation from Relations

Authors: Ulysse Gérard and Dale Miller

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

The logical foundation of arithmetic generally starts with a quantificational logic over relations. Of course, one often wishes to have a formal treatment of functions within this setting. Both Hilbert and Church added choice operators (such as the epsilon operator) to logic in order to coerce relations that happen to encode functions into actual functions. Others have extended the term language with confluent term rewriting in order to encode functional computation as rewriting to a normal form. We take a different approach that does not extend the underlying logic with either choice principles or with an equality theory. Instead, we use the familiar two-phase construction of focused proofs and capture functional computation entirely within one of these phases. As a result, our logic remains purely relational even when it is computing functions.

Cite as

Ulysse Gérard and Dale Miller. Separating Functional Computation from Relations. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 23:1-23:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

  author =	{G\'{e}rard, Ulysse and Miller, Dale},
  title =	{{Separating Functional Computation from Relations}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.23},
  URN =		{urn:nbn:de:0030-drops-77040},
  doi =		{10.4230/LIPIcs.CSL.2017.23},
  annote =	{Keywords: focused proof systems, fixed points, computation and deduction}
  • Refine by Author
  • 1 Gérard, Ulysse
  • 1 Miller, Dale

  • Refine by Classification

  • Refine by Keyword
  • 1 computation and deduction
  • 1 fixed points
  • 1 focused proof systems

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2017

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail