Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data.

Jay A. McCarthy

dblp:60/1832 · DBLP profile ↗
← Back
10ranked-venue papers
5as first author
1since 2021 · last 2023
0000-0002-2061-7396ORCID · reported

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 7 · 3 first-author · 1 since 2021Security and privacy · 1 · 1 first-authorDatabases, data management, data science and information retrieval · 1 · 1 first-authorHuman-computer interaction and ubiquitous computing · 1Applied, interdisciplinary, general and emerging computing · 1 · 1 first-author

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
3 papers
Programming languages and type systems · 94% Runtime systems and virtual machines · 4% Concurrent programming · 1%
Network and information security
1 paper
Authentication and access control · 77% Web and mobile security · 23%

Topics — the 7 heaviest of 10, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Programming languages and type systems
extensibility
0.712023
Rhombus: A New Spin on Macros without All the Parentheses · Proc. ACM Program. Lang. 2023
Programming languages and type systems › metaprogramming
macro systems
0.712023
Rhombus: A New Spin on Macros without All the Parentheses · Proc. ACM Program. Lang. 2023
Programming languages and type systems
metaprogramming
0.212023
Rhombus: A New Spin on Macros without All the Parentheses · Proc. ACM Program. Lang. 2023
Programming languages and type systems › language semantics
formal semantics
0.112012
Run your research: on the effectiveness of lightweight mechanization · POPL 2012
Programming languages and type systems › control operators
continuations
0.112010
The two-state solution: native and serializable continuations accord · OOPSLA 2010
Authentication and access control
trust management
0.112007
Compiling cryptographic protocols for deployment on the web · WWW 2007
Concurrent programming › concurrency control
serializability
0.012010
The two-state solution: native and serializable continuations accord · OOPSLA 2010

Methods — techniques the papers use, named apart from their topics

macro expansion protocol · 0.7proof assistant · 0.1serialization · 0.1continuation capture · 0.1
YearPublicationVenuePosition
2023 Rhombus: A New Spin on Macros without All the Parentheses
abstract
Rhombus is a new language that is built on Racket. It offers the same kind of language extensibility as Racket itself, but using traditional (infix) notation. Although Rhombus is far from the first language to support Lisp-style macros without Lisp-style parentheses, Rhombus offers a novel synthesis of macro technology that is practical and expressive. A key element is the use of multiple binding spaces for context-specific sublanguages. For example, expressions and pattern-matching forms can use the same operators with different meanings and without creating conflicts. Context-sensitive bindings, in turn, facilitate a language design that reduces the notational distance between the core language and macro facilities. For example, repetitions can be defined and used in binding and expression contexts generally, which enables a smoother transition from programming to metaprogramming. Finally, since handling static information (such as types) is also a necessary part of growing macros beyond Lisp, Rhombus includes support in its expansion protocol for communicating static information among bindings and expressions. The Rhombus implementation demonstrates that all of these pieces can work together in a coherent and user-friendly language.
Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay A. McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, Sam Tobin-Hochstadt
Proc. ACM Program. Lang.11
2018 A Coq library for internal verification of running-times
Jay A. McCarthy, Burke Fetscher, Max S. New, Daniel Feltey, Robert Bruce Findler
Sci. Comput. Program.1
2017 Fair enumeration combinators
abstract
Abstract Enumerations represented as bijections between the natural numbers and elements of some given type have recently garnered interest in property-based testing because of their efficiency and flexibility. There are, however, many ways of defining these bijections, some of which are better than others. This paper offers a new property of enumeration combinators called fairness that identifies enumeration combinators that are better suited to property-based testing. Intuitively, the result of a fair combinator indexes into its argument enumerations equally when constructing its result. For example, extracting the n th element from our enumeration of three-tuples indexes about $\sqrt[3]{n}$ elements into each of its components instead of, say, indexing $\sqrt[2]{n}$ into one and $\sqrt[4]{n}$ into the other two, as you would if a three-tuple were built out of nested pairs. Similarly, extracting the n th element from our enumeration of a three-way union returns an element that is $\frac{n}{3}$ into one of the argument enumerators. The paper presents a semantics of enumeration combinators, a theory of fairness, proofs establishing fairness of our new combinators and that some combinations of fair combinators are not fair. We also report on an evaluation of fairness for the purpose of finding bugs in programming-language models. We show that fair enumeration combinators have complementary strengths to an existing, well-tuned ad hoc random generator (better on short time scales and worse on long time scales) and that using unfair combinators is worse across the board.
Max S. New, Burke Fetscher, Robert Bruce Findler, Jay A. McCarthy
J. Funct. Program.4
2013 Teaching garbage collection without implementing compiler or interpreters
abstract
Given the widespread use of memory-safe languages, students must understand garbage collection well. Following a constructivist philosophy, an effective approach would be to have them implement garbage collectors. Unfortunately, a full implementation depends on substantial knowledge of compilers and runtime systems, which many courses do not cover or cannot assume.
Gregory H. Cooper, Arjun Guha, Shriram Krishnamurthi, Jay A. McCarthy, Robert Bruce Findler
SIGCSE4
2012 Run your research: on the effectiveness of lightweight mechanization
abstract
Formal models serve in many roles in the programming language community. In its primary role, a model communicates the idea of a language design; the architecture of a language tool; or the essence of a program analysis. No matter which role it plays, however, a faulty model doesn't serve its purpose.
Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, Robert Bruce Findler
POPL7
2011 A Semantics for Context-Sensitive Reduction Semantics
Casey Klein, Jay A. McCarthy, Steven Jaconette, Robert Bruce Findler
APLAS2
2010 The two-state solution: native and serializable continuations accord
abstract
Continuation-based Web servers provide advantages over traditional Web application development through the increase of expressive power they allow. This leads to fewer errors and more productivity for the programmers that adopt them. Unfortunately, existing implementation techniques force a hard choice between scalability and expressiveness.
Jay A. McCarthy
OOPSLA1
2009 Automatically RESTful web applications: marking modular serializable continuations
abstract
Continuation-based Web servers provide distinct advantages over traditional Web application development: expressive power and modularity. This power leads to fewer errors and more interesting applications. Furthermore, these Web servers are more than prototypes; they are used in some real commercial applications. Unfortunately, they pay a heavy price for the additional power in the form of lack of scalability.
Jay A. McCarthy
ICFP1
2008 Cryptographic Protocol Explication and End-Point Projection
Jay A. McCarthy, Shriram Krishnamurthi
ESORICS1
2007 Compiling cryptographic protocols for deployment on the web
abstract
Cryptographic protocols are useful for trust engineering in Web transactions. The Cryptographic Protocol Programming Language (CPPL) provides a model wherein trust management annotations are attached to protocol actions, and are used to constrain the behavior of a protocol participant to be compatible with its own trust policy.
Jay A. McCarthy, Shriram Krishnamurthi, Joshua D. Guttman, John D. Ramsdell
WWW1