jason-gross.bib

@misc{2014-msr-x86proved-io,
  author = {Jason Gross},
  title = {Presentation: Input, Output, and Automation in x86 Proved},
  month = {August},
  year = {2014},
  note = {Presented at Microsoft Research, Cambridge, UK},
  abstract = {The x86proved project can now verify assembly programs with input
	and output! The code-reasoning throughout the project is now mostly
	automatic. Although not yet push-button verification (specification-level
	reasoning, in particular, leaves a lot to be desired) these tactics
	make a significant step towards that goal. This presentation will
	cover: \\ • some programs whose I/O behaviour has been verified (including
	a simplified version of the \texttt{echo} command-line tool) \\ •
	the new automation for fully automatic correctness proofs of Hoare-triple
	rules for basic instructions \\ • the new automation for applying
	Hoare rules for assembly instructions automatically \\ • the basics
	of how we're specifying and verifying the I/O behaviour of programs},
  day = {20},
  owner = {Jason},
  timestamp = {2014.08.20},
  url = {https://people.csail.mit.edu/jgross/personal-website/presentations/msr-2014-final-talk/input-output-and-automation-in-x86proved.pdf},
  url-pptx = {https://people.csail.mit.edu/jgross/personal-website/presentations/msr-2014-final-talk/input-output-and-automation-in-x86proved.pptx}
}
@inproceedings{adt-synthesis,
  author = {Ben Delaware and Cl\'ement Pit--Claudel and Jason Gross and Adam
	Chlipala},
  title = {Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant},
  booktitle = {Proceedings of the \href{http://popl.mpi-sws.org/2015/}{42nd ACM
	SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'15)}},
  year = {2015},
  month = {January},
  abstract = {We present Fiat, a library for the Coq proof assistant supporting
	refinement of declarative specifications into efficient functional
	programs with a high degree of automation. Each refinement process
	leaves a proof trail, checkable by the normal Coq kernel, justifying
	its soundness. We focus on the synthesis of abstract data types that
	package methods with private data. We demonstrate the utility of
	our framework by applying it to the synthesis of \textit{query structures}
	-- abstract data types with SQL-like query and insert operations.
	Fiat includes a library for writing specifications of query structures
	in SQL-inspired notation, expressing operations over relations (tables)
	in terms of mathematical sets. This library includes a set of tactics
	for automating the refinement of these specifications into efficient,
	correct-by-construction OCaml code. Using these tactics, a programmer
	can generate such an implementation completely automatically by only
	specifying the equivalent of SQL indexes, data structures capturing
	useful views of the abstract data. We conclude by speculating on
	the new programming modularity possibilities enabled by an automated
	refinement system with proved-correct rules.},
  acm-authorize-url = {https://dl.acm.org/authorize?N20774},
  owner = {Jason},
  timestamp = {2014.10.07},
  url = {https://people.csail.mit.edu/jgross/personal-website/papers/2015-adt-synthesis.pdf}
}
@inproceedings{Bauer:2017:HLF:3018610.3018615,
  author = {Bauer, Andrej and Gross, Jason and Lumsdaine, Peter LeFanu and Shulman, Michael and Sozeau, Matthieu and Spitters, Bas},
  title = {The {HoTT} Library: A Formalization of Homotopy Type Theory in {C}oq},
  booktitle = {Proceedings of the \href{http://cpp2017.mpi-sws.org/}{6th ACM SIGPLAN Conference on Certified Programs and Proofs}},
  year = {2017},
  series = {CPP 2017},
  pages = {164--172},
  address = {New York, NY, USA},
  month = {January},
  publisher = {ACM},
  abstract = {We report on the development of the \emph{{HoTT} library}, a formalization of homotopy type theory in the {Coq} proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of {Coq}, such as universe polymorphism and private inductive types.},
  acmid = {3018615},
  doi = {10.1145/3018610.3018615},
  eprint = {1610.04591},
  isbn = {978-1-4503-4705-1},
  keywords = {Coq, Higher inductive types, Homotopy type theory, Univalent foundations, Universe polymorphism},
  location = {Paris, France},
  numpages = {9},
  oai2identifier = {1610.04591},
  url = {https://people.csail.mit.edu/jgross/personal-website/papers/2017-HoTT-formalization.pdf}
}
@inproceedings{category-coq-experience,
  author = {Jason Gross and Adam Chlipala and David I. Spivak},
  title = {Experience Implementing a Performant Category-Theory Library in {C}oq},
  booktitle = {Proceedings of the \href{http://www.cs.uwyo.edu/~ruben/itp-2014}{5th
	International Conference on Interactive Theorem Proving (ITP'14)}},
  year = {2014},
  month = {July},
  abstract = {We describe our experience implementing a broad category-theory library
	in Coq. Category theory and computational performance are not usually
	mentioned in the same breath, but we have needed substantial engineering
	effort to teach Coq to cope with large categorical constructions
	without slowing proof script processing unacceptably. In this paper,
	we share the lessons we have learned about how to represent very
	abstract mathematical objects and arguments in Coq and how future
	proof assistants might be designed to better support such reasoning.
	One particular encoding trick to which we draw attention allows category-theoretic
	arguments involving \emph{duality} to be internalized in Coq's logic
	with definitional equality. Ours may be the largest Coq development
	to date that uses the relatively new Coq version developed by homotopy
	type theorists, and we reflect on which new features were especially
	helpful.},
  eprint = {1401.7694},
  full-bibliography = {https://people.csail.mit.edu/jgross/personal-website/papers/category-coq-experience.html},
  original-url = {https://people.csail.mit.edu/jgross/personal-website/papers/category-coq-experience-itp-submission.pdf},
  owner = {Jason},
  presentation-annotated-pptx = {https://people.csail.mit.edu/jgross/personal-website/presentations/itp-2014/category-coq-experience.pptx},
  presentation-pdf = {https://people.csail.mit.edu/jgross/personal-website/presentations/itp-2014/category-coq-experience.pdf},
  published-url-springer = {http://link.springer.com/chapter/10.1007/978-3-319-08970-6_18},
  reviews = {https://people.csail.mit.edu/jgross/personal-website/papers/category-coq-experience-itp-2014-reviews.txt},
  timestamp = {2014.01.19},
  url = {https://people.csail.mit.edu/jgross/personal-website/papers/category-coq-experience-itp-submission-final.pdf}
}
@misc{coqpl-15-coq-bug-minimizer,
  author = {Jason Gross},
  title = {Coq Bug Minimizer},
  month = {January},
  year = {2015},
  note = {Presented at \href{https://coqpl.cs.washington.edu/2014/07/31/}{The First International Workshop on Coq for PL (CoqPL'15)}},
  abstract = {Are bugs the bane of your existence? Do you dread Coq upgrades, because
	they mean you'll have to spend days tracking down subtle failures
	deep in your developments? Have you ever hit an anomaly that just
	wouldn't go away, and wished you understood what triggered it? Have
	you ever been tormented by two blocks of code that looked identical,
	but behaved differently? Do you wish you submit more helpful error
	reports, but don't want to put in the time to construct minimal examples?
	If you answered ``yes'' to any of these questions, then the Coq Bug
	Minimizer is for you! Clone your own copy at \url{https://github.com/JasonGross/coq-bug-finder}.},
  owner = {Jason},
  reviews = {https://people.csail.mit.edu/jgross/personal-website/papers/2015-coq-bug-minimizer-reviews.txt},
  timestamp = {2014.10.07},
  url = {https://people.csail.mit.edu/jgross/personal-website/papers/2015-coq-bug-minimizer.pdf}
}
@misc{coqpl-15-ltac-profiler,
  author = {Tobias Tebbi and Jason Gross},
  title = {A Profiler for {L}tac},
  month = {January},
  year = {2015},
  note = {Presented at \href{https://coqpl.cs.washington.edu/2014/07/31/}{The First International Workshop on Coq for PL (CoqPL'15)}},
  abstract = {We present a simple profiler for the Ltac tactic language of the Coq
	Proof Assistent. It measures the time spent in invocations of primitive
	tactics as well as tactics defined in Ltac and their inner invocations.
	The profiler is controlled using Vernacular commands and prints an
	aggregated view that differentiates between tactic invocations depending
	on their call tree location.},
  owner = {Jason},
  timestamp = {2014.10.17},
  url = {https://people.csail.mit.edu/jgross/personal-website/papers/2015-ltac-profiler.pdf}
}
@misc{Gross2013a-database-in-categories,
  author = {Jason Gross},
  title = {Building Database Management on top of Category Theory in {C}oq},
  month = {January},
  year = {2013},
  owner = {Jason},
  note = {Presented as a student talk at the \href{http://popl.mpi-sws.org/2013/}{40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13)}},
  timestamp = {2014.01.21},
  url = {https://people.csail.mit.edu/jgross/personal-website/presentations/popl-2013/jgross-student-talk.pdf}
}
@misc{Gross2013b-popl-minute-madness,
  author = {Jason Gross},
  title = {{POPL}: Minute Madness: Database Management on top of Category Theory
	in {C}oq: Category of Relational Schemas = Category of Categories},
  month = {January},
  year = {2013},
  owner = {Jason},
  note = {Presented at the \href{http://popl.mpi-sws.org/2013/}{40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13)}},
  timestamp = {2014.01.21},
  url = {https://people.csail.mit.edu/jgross/personal-website/presentations/popl-2013/minute-madness.pdf}
}
@misc{Gross2013-csw,
  author = {Jason Gross},
  title = {{CSAIL} Student Workshop 2013: Computational Higher Inductive Types:
	Computing with Custom Equalities},
  month = {October},
  year = {2013},
  note = {Presented at the \href{http://projects.csail.mit.edu/csw/2014/index.htm}{2014 MIT CSAIL Student Workshop}},
  owner = {Jason},
  timestamp = {2014.01.21},
  url = {https://people.csail.mit.edu/jgross/personal-website/presentations/csw-2013/jgross-presentation-no-pause.pdf}
}
@misc{Gross2014a-coq-wishlist,
  author = {Jason Gross},
  title = {{J}ason {G}ross' Wishlist for {C}oq},
  month = {January},
  year = {2014},
  owner = {Jason},
  timestamp = {2014.01.21},
  url = {https://people.csail.mit.edu/jgross/personal-website/presentations/coq-8.6-wishlist/jgross-coq-8-6-wishlist-no-pause.pdf}
}
@misc{Gross2014b-popl-minute-madness,
  author = {Jason Gross},
  title = {{POPL}: Minute Madness: Category Theory in {C}oq, and Program Synthesis},
  month = {January},
  year = {2014},
  owner = {Jason},
  note = {Presented at the \href{http://popl.mpi-sws.org/2014/}{41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14)}},
  timestamp = {2014.01.21},
  url = {https://people.csail.mit.edu/jgross/personal-website/presentations/popl-2014-minute-madness/jason-gross-minute-madness.pdf}
}
@misc{Gross2014c-coq-workshop-proposal,
  author = {Jason Gross},
  title = {Presentation Proposal for of Three Neat Tricks in {C}oq 8.5},
  month = {April},
  year = {2014},
  note = {Presented at the \href{http://www.easychair.org/smart-program/VSL2014/Coq-index.html}{6th Coq Workshop}},
  abstract = {Coq 8.5 has a number of new features. It has more powerful universe
	polymorphism support. It allows tactics to be run at interpretation
	to construct other terms. The ability to switch from Gallina to Ltac
	in arbitrary locations nicely complements the \texttt{constr:}~notation
	permitting the switch from Ltac to Gallina in tactics, and opens
	up many new possibilities. I propose to present three tricks involving
	these new features: tactics in terms allows the construction of tactics
	that recurse under binders; tactics in terms together with typeclasses
	allows overloading notations based on the type of their arguments;
	and there is a way to talk about universe levels explicitly, helped
	along by tactics in terms.},
  code-html = {https://people.csail.mit.edu/jgross/personal-website/presentations/coq-workshop-2014/html/CoqWorkshop.tactics_in_terms_presentation.html},
  code-v = {https://people.csail.mit.edu/jgross/personal-website/presentations/coq-workshop-2014/tactics_in_terms_presentation.v},
  day = {11},
  owner = {Jason},
  reviews = {https://people.csail.mit.edu/jgross/personal-website/presentations/coq-workshop-2014/reviews.txt},
  timestamp = {2014.04.11},
  url = {https://people.csail.mit.edu/jgross/personal-website/presentations/coq-workshop-2014/coq-workshop-proposal-tactics-in-terms.pdf}
}
@misc{hott-hott-and-category-coq-experience,
  author = {Jason Gross},
  title = {The {HoTT}/{HoTT} Library in {C}oq: Designing for Speed},
  month = {July},
  year = {2016},
  note = {Presented at \href{http://icms2016.zib.de/}{The 5th International Congress on Mathematical Software (ICMS 2016)}},
  abstract = {The HoTT/HoTT library is one of the major Coq libraries exploring univalent foundations and homotopy type theory, the other being UniMath.  The library includes formalization of the basic type formers, some axiomatic higher inductive types including the circle, the interval, suspensions, and quotients, a formalization of modalities (reflective subtoposes) using modules as a way to quantify over all universe levels, formalizations of Cantor spaces and the surreals, the basic theory of h-levels, and a significant amount of category theory centered around comma categories and functoriality of various constructions involving comma categories.  A significant amount of work has gone into ensuring that the library compiles quickly.  This talk will discuss the various constructions in the HoTT library, as well as the design choices and features, both of Coq and of univalent type theory, which allow our library to compile and typecheck quickly.},
  owner = {Jason},
  presentation-annotated-pptx = {https://people.csail.mit.edu/jgross/personal-website/presentations/icms-2016/hott-hott-and-category-coq-experience.pptx},
  url = {https://people.csail.mit.edu/jgross/personal-website/presentations/icms-2016/hott-hott-and-category-coq-experience.pdf}
}
@mastersthesis{jgross-thesis,
  author = {Jason Gross},
  title = {An Extensible Framework for Synthesizing Efficient, Verified Parsers},
  school = {Massachusetts Institute of Technology},
  year = {2015},
  month = {September},
  abstract = {Parsers have a long history in computer science. This thesis proposes a novel approach to synthesizing efficient, verified parsers by refinement, and presents a demonstration of this approach in the Fiat framework by synthesizing a parser for arithmetic expressions.  The benefits of this framework may include more flexibility in the parsers that can be described, more control over the low-level details when necessary for performance, and automatic or mostly automatic correctness proofs.},
  url = {https://people.csail.mit.edu/jgross/personal-website/papers/2015-jgross-thesis.pdf}
}
@inproceedings{Lake2011,
  author = {Brenden M. Lake and Ruslan Salakhutdinov and Jason Gross and Joshua
	B. Tenenbaum},
  title = {One shot learning of simple visual concepts},
  booktitle = {Proceedings of the \href{http://cognitivesciencesociety.org/conference2011/index.html}{33rd Annual Conference of the Cognitive Science
	Society}},
  year = {2011},
  abstract = {People can learn visual concepts from just one example, but it remains
	a mystery how this is accomplished. Many authors have proposed that
	transferred knowledge from more familiar concepts is a route to one
	shot learning, but what is the form of this abstract knowledge? One
	hypothesis is that the sharing of parts is core to one shot learning,
	and we evaluate this idea in the domain of handwritten characters,
	using a massive new dataset. These simple visual concepts have a
	rich internal part structure, yet they are particularly tractable
	for computational models. We introduce a generative model of how
	characters are composed from strokes, where knowledge from previous
	characters helps to infer the latent strokes in novel characters.
	The stroke model outperforms a competing state-of-the-art character
	model on a challenging one shot learning task, and it provides a
	good fit to human perceptual data.},
  owner = {Jason},
  timestamp = {2014.01.19},
  url = {https://people.csail.mit.edu/jgross/personal-website/papers/LakeEtAl2011CogSci.pdf},
  videos = {https://people.csail.mit.edu/jgross/personal-website/media/charactervideos.html}
}

This file was generated by bibtex2html 1.97.