Fetching the paper…
Reading the bibliography…
We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming.
Synthesizing proofs from programs in the calculus of inductive constructions
Catherine Parent · 1995
Earlier work this paper cites.
Definitional Interpreters for Higher-Order Programming Languages
John C. Reynolds · 1998
Earlier work this paper cites.
Subset coercions in Coq
Matthieu Sozeau · 2007
Earlier work this paper cites.
A Certified Implementation of ML with Structural Polymorphism
Jacques Garrigue · 2010
Earlier work this paper cites.
Engineering proof by reflection in Agda
Paul van der Walt and Wouter Swierstra · 2013
Earlier work this paper cites.
System fc with explicit kind equality
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg · 2013
Earlier work this paper cites.
Elaborator Reflection: Extending Idris in Idris
David Christiansen and Edwin Brady · 2016
Earlier work this paper cites.
Making Smart Contracts Smarter
Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor · 2016
Earlier work this paper cites.
Type Soundness Proofs with Definitional Interpreters
Nada Amin and Tiark Rompf · 2017
Earlier work this paper cites.
CertiCoq: A verified compiler for Coq
Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Belanger, Matthieu Sozeau, and Matthew Weaver · 2017
Cited alongside, same era.
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura · 2017
Cited alongside, same era.
Simplicity: A New Language for Blockchains
Russell O’Connor · 2017
Cited alongside, same era.
A Concurrent Perspective on Smart Contracts
Ilya Sergey and Aquinas Hobor · 2017
Cited alongside, same era.
A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq
Niki Vazou, Leonidas Lampropoulos, and Jeff Polakow · 2017
Cited alongside, same era.
Towards Certified Meta-Programming with Typed Template-Coq
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau · 2018
Total Haskell is Reasonable Coq
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich · 2018
Later among the works it cites.
Equivalences for Free: Univalent Parametricity for Effective Transport
Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau · 2018
Later among the works it cites.
Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts
Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Zhenlei Pesin, and Julien Tesson · 2019
Closest in time.
System F in Agda, for fun and profit
James Chapman, Roman Kireev, Chad Nester, and Philip Wadler · 2019
Closest in time.
A certifying extraction with time bounds from Coq to call-by-value λ \lambda -calculus
Yannick Forster and Fabian Kunze · 2019
Closest in time.
Smart Contract Interactions in Coq
Jakob Botsch Nielsen and Bas Spitters · 2019
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Revisiting Parametricity: Inductives and Uniformity of Propositions
Abhishek Anand and Greg Morrisett · 2018
Cited alongside, same era.
Liquidity: OCaml pour la Blockchain
Çagdas Bozman, Mohamed Iguernlala, Michael Laporte, Fabrice Le Fessant, and Alain Mebsout · 2018
Cited alongside, same era.
Scilla: a Smart Contract Intermediate-Level LAnguage
Ilya Sergey, Amrit Kumar, and Aquinas Hobor · 2018
Cited alongside, same era.
System F Omega
András Kovács
Cited in the paper.
A formalization of the polymorphic lambda calculus extended with iso-recursive types
Sandro Stucki
Cited in the paper.
Closest in time.
Unraveling recursion: compiling an IR with recursion to System F
Michael Peyton Jones, Vasilis Gkoumas, Roman Kireev, Kenneth MacKenzie, Chad Nester, and Philip Wadler · 2019
Closest in time.
Safer Smart Contract Programming with Scilla
Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan · 2019
Closest in time.