4 Search Results for "Ko, Andrew J."


Document
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
Human-Centric Development of Software Tools (Dagstuhl Seminar 15222)

Authors: Andrew J. Ko, Shriram Krishnamurthi, Gail C. Murphy, and Janet Siegmund

Published in: Dagstuhl Reports, Volume 5, Issue 5 (2016)


Abstract
Over two and half days, over 30 participants engaged in inventing and evaluating programming and software engineering tools from a human rather than tool perspective. We discussed methods, theories, recruitment, research questions, and community issues such as methods training and reviewing. This report is a summary of the key insights generated in the workshop.

Cite as

Andrew J. Ko, Shriram Krishnamurthi, Gail C. Murphy, and Janet Siegmund. Human-Centric Development of Software Tools (Dagstuhl Seminar 15222). In Dagstuhl Reports, Volume 5, Issue 5, pp. 115-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{ko_et_al:DagRep.5.5.115,
  author =	{Ko, Andrew J. and Krishnamurthi, Shriram and Murphy, Gail C. and Siegmund, Janet},
  title =	{{Human-Centric Development of Software Tools (Dagstuhl Seminar 15222)}},
  pages =	{115--132},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{5},
  editor =	{Ko, Andrew J. and Krishnamurthi, Shriram and Murphy, Gail C. and Siegmund, Janet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.5.115},
  URN =		{urn:nbn:de:0030-drops-54049},
  doi =		{10.4230/DagRep.5.5.115},
  annote =	{Keywords: Software engineering, developer tools, human factors}
}
Document
Computing and Diagnosing Changes in Unit Test Energy Consumption

Authors: Andrew J. Ko, Michal Young, Jamie Andrews, Brian P. Robinson, and Mark Grechanik

Published in: Dagstuhl Seminar Proceedings, Volume 10111, Practical Software Testing : Tool Automation and Human Factors (2010)


Abstract
Many developers have reason to be concerned with with power consumption. For example, mobile app developers want to minimize how much power their applications draw, while still providing useful functionality. However, developers have few tools to get feedback about changes to their application's power consumption behavior as they implement an application and make changes to it over time. We present a tool that, using a team's existing test cases, performs repeated measurements of energy consumption based on instructions executed, objects generated, and blocking latency, generating a distribution of energy use estimates for each test run, recording these distributions in a time series of distributions over time. Then, when these distributions change substantially, we inform the developer of this change, and offer them diagnostic information about the elements of their code potentially responsible for the change and the inputs responsible. Through this information, we believe that developers will be better enabled to relate recent changes in their code to changes in energy consumption, enabling them to better incorporate changes in software energy consumption into their software evolution decisions.

Cite as

Andrew J. Ko, Michal Young, Jamie Andrews, Brian P. Robinson, and Mark Grechanik. Computing and Diagnosing Changes in Unit Test Energy Consumption. In Practical Software Testing : Tool Automation and Human Factors. Dagstuhl Seminar Proceedings, Volume 10111, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{ko_et_al:DagSemProc.10111.4,
  author =	{Ko, Andrew J. and Young, Michal and Andrews, Jamie and Robinson, Brian P. and Grechanik, Mark},
  title =	{{Computing and Diagnosing Changes in Unit Test Energy Consumption}},
  booktitle =	{Practical Software Testing : Tool Automation and Human Factors},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10111},
  editor =	{Mark Harman and Henry Muccini and Wolfram Schulte and Tao Xie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10111.4},
  URN =		{urn:nbn:de:0030-drops-26248},
  doi =		{10.4230/DagSemProc.10111.4},
  annote =	{Keywords: Energy, oracles}
}
Document
Barriers to Successful End-User Programming

Authors: Andrew J. Ko

Published in: Dagstuhl Seminar Proceedings, Volume 7081, End-User Software Engineering (2007)


Abstract
In my research and my personal life, I have come to know numerous people that our research community might call end-user programmers. Some of them are scientists, some are artists, others are educators and other types of professionals. One thing that all of these people have in common is that their goals are entirely unrelated to producing code. In some cases, programming may be a necessary part of accomplishing their goals, such as a physicist writing a simulation in C or an interaction designer creating an interactive prototype. In other cases, programming may simply be the more efficient alternative to manually solving a problem: one might find duplicate entries in an address book by visual search or by writing a short Perl script.

Cite as

Andrew J. Ko. Barriers to Successful End-User Programming. In End-User Software Engineering. Dagstuhl Seminar Proceedings, Volume 7081, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{ko:DagSemProc.07081.4,
  author =	{Ko, Andrew J.},
  title =	{{Barriers to Successful End-User Programming}},
  booktitle =	{End-User Software Engineering},
  pages =	{1--1},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7081},
  editor =	{Margaret H. Burnett and Gregor Engels and Brad A. Myers and Gregg Rothermel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07081.4},
  URN =		{urn:nbn:de:0030-drops-10913},
  doi =		{10.4230/DagSemProc.07081.4},
  annote =	{Keywords: End-user programming, learning, empirical studies}
}
  • Refine by Author
  • 3 Ko, Andrew J.
  • 1 Andrews, Jamie
  • 1 Grechanik, Mark
  • 1 Grossman, Dan
  • 1 Krishnamurthi, Shriram
  • Show More...

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

  • Refine by Keyword
  • 1 End-user programming
  • 1 Energy
  • 1 Software engineering
  • 1 developer tools
  • 1 empirical studies
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2007
  • 1 2010
  • 1 2016
  • 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