4 citations · 9 across the 5 of their papers we have counts for
7 papers
Substructural Parametricity
C. B. Aberlé, Chris Martens, Frank Pfenning
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary lo…
Verifying the Hashgraph Consensus Algorithm
Karl Crary
The Hashgraph consensus algorithm is an algorithm for asynchronous Byzantine fault tolerance intended for distributed shared ledgers. Its main distinguishing characteristic is it a…
Compiling a Calculus for Relaxed Memory: Practical constraint-based low-level concurrency
Michael J. Sullivan, Karl Crary, Salil Joshi
Crary and Sullivan's Relaxed Memory Calculus (RMC) proposed a new declarative approach for writing low-level shared memory concurrent programs in the presence of modern relaxed-mem…
Hygienic Source-Code Generation Using Functors
Karl Crary
Existing source-code-generating tools such as Lex and Yacc suffer from practical inconveniences because they use disembodied code to implement actions. To prevent this problem, suc…
TWAM: A Certifying Abstract Machine for Logic Programs
Rose Bohrer, Karl Crary
Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a type-preserving compiler for a s…
Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice
Karl Crary, Marino Miculan
Type theories, logical frameworks and meta-languages form a common foundation for designing, implementing, and reasoning about formal languages and their semantics. They are centra…
Logic Column 16: Higher-Order Abstract Syntax: Setting the Record Straight
Karl Crary, Robert Harper
This article responds to a critique of higher-order abstract syntax appearing in Logic Column 14, ``Nominal Logic and Abstract Syntax'', cs.LO/0511025.