proof assistant - researchr tag

researchr

You are not signed in
Sign in
Sign up

2011

2010

A verified compiler for an impure functional languageAdam J. Chlipala. POPL 2010: 93-106 [doi]

Proof Assistants as Teaching Assistants: A View from the TrenchesBenjamin C. Pierce. itp 2010: 8 [doi]

Ott: Effective tool support for the working semanticistPeter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strnisa. JFP, 20(1):71-122, 2010. [doi]

Bringing extensibility to verified compilersZachary Tatlock, Sorin Lerner. PLDI 2010: 111-121 [doi]

A Machine-Checked Proof for a Product-Line-Aware Type SystemThomas Thüm. Master's thesis, University of Magdeburg, Germany, January 2010.

Formal polytypic programs and proofsWendy Verbruggen, Edsko de Vries, Arthur Hughes. JFP, 20(3-4):213-269, 2010. [doi]

2009

2008

On the Algebraic Foundation of Proof Assistants for Intuitionistic Type TheoryAndreas Abel, Thierry Coquand, Peter Dybjer. FLOPS 2008: 3-13 [doi]

Engineering formal metatheoryBrian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich. POPL 2008: 3-15 [doi]

Modular development of certified program verifiers with a proof assistant, Adam J. Chlipala. JFP, 18(5-6):599-647, 2008. [doi]

Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008Piotr Rudnicki, Geoff Sutcliffe, Boris Konev, Renate A. Schmidt, Stephan Schulz, editors, Volume 418 of CEUR Workshop Proceedings, CEUR-WS.org, 2008.

Galculator : functional prototype of a Galois-connection based proof assistantPaulo F. Silva, José Nuno Oliveira. ppdp 2008: 44-55 [doi]

Modeling and Verifying Graph Transformations in Proof AssistantsMartin Strecker. ENTCS, 203(1):135-148, 2008. [doi]

Polytypic programming in COQWendy Verbruggen, Edsko de Vries, Arthur Hughes. ICFP 2008: 49-60 [doi]

2007

Web Interfaces for Proof AssistantsENTCS, 174(2):49-61, 2007. [doi]

Formal Proof of Provable Security by Game-Playing in a Proof AssistantReynald Affeldt, Miki Tanaka, Nicolas Marti. provsec 2007: 151-168 [doi]

User Interaction with the Matita Proof AssistantAndrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. JAR, 39(2):109-139, 2007. [doi]

Position Paper: Thoughts on Programming with Proof AssistantsAdam J. Chlipala. ENTCS, 174(7):17-21, 2007. [doi]

A Declarative Language for the Coq Proof AssistantPierre Corbineau. TYPES 2008: 69-84 [doi]

A Single-Step Term-Graph Reduction System for Proof AssistantsMaarten de Mol, Marko C. J. D. van Eekelen, Marinus J. Plasmeijer. agtive 2008: 184-200 [doi]

Ott: effective tool support for the working semanticistPeter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa. ICFP 2007: 1-12 [doi]

2006

Crafting a Proof AssistantAndrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. TYPES 2007: 18-32 [doi]

SAEPTUM: verification of ::::ELAN:::: hardware specifications using the proof assistant ::::PVS::::Mauricio Ayala-Rincón, Thomas Mailleux Santana. sbcci 2006: 125-130 [doi]

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof AssistantGilles Barthe, Julien Forest, David Pichardie, Vlad Rusu. FLOPS 2006: 114-129 [doi]

Modular development of certified program verifiers with a proof assistantAdam J. Chlipala. ICFP 2006: 160-171 [doi]

Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra SystemDavid Delahaye, Micaela Mayero. ENTCS, 151(1):57-73, 2006. [doi]

A proof-centric approach to mathematical assistantsLucas Dixon, Jacques D. Fleuriot. japll, 4(4):505-532, 2006. [doi]

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof AssistantsPascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu. TACAS 2006: 167-181 [doi]

Formal certification of a compiler back-end or: programming a compiler with a proof assistantXavier Leroy. POPL 2006: 42-54 [doi]

2005

2004

Extracting a Data Flow Analyser in Constructive LogicDavid Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu. ESOP 2004: 385-400 [doi]

Mathematical Libraries as Proof Assistant EnvironmentsClaudio Sacerdoti Coen. mkm 2004: 332-346 [doi]

Thoughts on Requirements and Design Issues of User Interfaces for Proof AssistantsNorbert Völker. ENTCS, 103:139-159, 2004. [doi]

2003

2002

Proving Self-Stabilization with a Proof AssistantPierre Courtieu. ipps 2002: [doi]

External Rewriting for Skeptical Proof AssistantsQuang Huy Nguyen, Claude Kirchner, Hélène Kirchner. JAR, 29(3-4):309-336, 2002.

Isabelle/HOL - A Proof Assistant for Higher-Order LogicTobias Nipkow, Lawrence C. Paulson, Markus Wenzel. Volume 2283 of Lecture Notes in Computer Science, Springer, 2002.

2001

Electronic Communication of Mathematics and the Interaction of Computer Algebra Systems and Proof AssistantsHenk Barendregt, Arjeh M. Cohen. JSC, 32(1/2):3-22, 2001.

Proof-Assistants Using Dependent Type SystemsHenk Barendregt, Herman Geuvers. In John Alan Robinson, Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes). pages 1149-1238, Elsevier and MIT Press, 2001.

JProver : Integrating Connection-Based Theorem Proving into Interactive Proof AssistantsStephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin. cade 2001: 421-426 [doi]

2000

Graphical Theories of Interactive Systems: Can a Proof Assistant Help?Robin Milner. tphol 2000: 442

Generalization in Type Theory Based Proof AssistantsOlivier Pons. TYPES 2002: 217-232 [doi]

1998

Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract)Kenneth L. McMillan. FMCAD 1998: 1 [doi]

1996

Experiences with Software Specification and Verification Using LP, The Larch Proof AssistantManfred Broy. fmsd, 8(3):221-272, 1996.

Design Proof Assistant (Abstract)Gérard P. Huet. RTA 1996: 153

1995

Algebraic Proof Assistants in HOLRix Groenboom, Chris Hendriks, Indra Polak, Jan Terlouw, Jan Tijmen Udding. mpc 1995: 304-321

MacKE: Yet Another Proof Assistant & Automated Pedagogic ToolJeremy V. Pitt. tableaux 1995: 324-337

1994

Towards a Duration Calculus Proof Assistant in PVSJens Ulrik Skakkebæk, Natarajan Shankar. ftrtft 1994: 660-679

1992

A Proof Assistant for Symbolic Model-CheckingJulian C. Bradfield. cav 1993: 316-329

1991

A Proof Assistant for PSFSjouke Mauw, Gert J. Veltink. cav 1992: 158-168

1985

CCS used as a proof-assistant toolChau Chun Hung. pstv 1985: 387-398