2 Search Results for "Leo, John"

Document
DOI: 10.4230/LIPIcs.ITP.2019.26
Ornaments for Proof Reuse in Coq

Authors: Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Ornaments express relations between inductive types with the same inductive structure. We implement fully automatic proof reuse for a particular class of ornaments in a Coq plugin, and show how such a tool can give programmers the rewards of using indexed inductive types while automating away many of the costs. The plugin works directly on Coq code; it is the first ornamentation tool for a non-embedded dependently typed language. It is also the first tool to automatically identify ornaments: To lift a function or proof, the user must provide only the source type, the destination type, and the source function or proof. In taking advantage of the mathematical properties of ornaments, our approach produces faster functions and smaller terms than a more general approach to proof reuse in Coq.
Cite as

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ringer_et_al:LIPIcs.ITP.2019.26,
  author =	{Ringer, Talia and Yazdani, Nathaniel and Leo, John and Grossman, Dan},
  title =	{{Ornaments for Proof Reuse in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{26:1--26:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.26},
  URN =		{urn:nbn:de:0030-drops-110816},
  doi =		{10.4230/LIPIcs.ITP.2019.26},
  annote =	{Keywords: ornaments, proof reuse, proof automation}
}
Document
DOI: 10.4230/OASIcs.ICCSW.2013.89
Dreaming Machines: On multimodal fusion and information retrieval using neural-symbolic cognitive agents

Authors: Leo de Penning, Artur D'Avila Garcez, and John-Jules C. Meyer

Published in: OASIcs, Volume 35, 2013 Imperial College Computing Student Workshop

Abstract
Deep Boltzmann Machines (DBM) have been used as a computational cognitive model in various AI-related research and applications, notably in computational vision and multimodal fusion. Being regarded as a biological plausible model of the human brain, the DBM is also becoming a popular instrument to investigate various cortical processes in neuroscience. In this paper, we describe how a multimodal DBM is implemented as part of a Neural-Symbolic Cognitive Agent (NSCA) for real-time multimodal fusion and inference of streaming audio and video data. We describe how this agent can be used to simulate certain neurological mechanisms related to hallucinations and dreaming and how these mechanisms are beneficial to the integrity of the DBM. Finally, we will explain how the NSCA is used to extract multimodal information from the DBM and provide a compact and practical iconographic temporal logic formula for complex relations between visual and auditory patterns.
Cite as

Leo de Penning, Artur D'Avila Garcez, and John-Jules C. Meyer. Dreaming Machines: On multimodal fusion and information retrieval using neural-symbolic cognitive agents. In 2013 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 35, pp. 89-94, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{depenning_et_al:OASIcs.ICCSW.2013.89,
  author =	{de Penning, Leo and D'Avila Garcez, Artur and Meyer, John-Jules C.},
  title =	{{Dreaming Machines: On multimodal fusion and information retrieval using neural-symbolic cognitive agents}},
  booktitle =	{2013 Imperial College Computing Student Workshop},
  pages =	{89--94},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-63-7},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{35},
  editor =	{Jones, Andrew V. and Ng, Nicholas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2013.89},
  URN =		{urn:nbn:de:0030-drops-42765},
  doi =		{10.4230/OASIcs.ICCSW.2013.89},
  annote =	{Keywords: Multimodal fusion, Deep Boltzmann Machine, Neural-Symbolic Cognitive Agent, Dreaming, Hallucinations}
}
  • Refine by Author
  • 1 D'Avila Garcez, Artur
  • 1 Grossman, Dan
  • 1 Leo, John
  • 1 Meyer, John-Jules C.
  • 1 Ringer, Talia
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Formal software verification

  • Refine by Keyword
  • 1 Deep Boltzmann Machine
  • 1 Dreaming
  • 1 Hallucinations
  • 1 Multimodal fusion
  • 1 Neural-Symbolic Cognitive Agent
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2013
  • 1 2019

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact