Jean-Paul Bodeveix - researchr profile publications

researchr

You are not signed in
Sign in
Sign up

[Clear Filters]

Publications tagged proof assistant

Isabelle as Document-Oriented Proof AssistantMakarius Wenzel. mkm 2011: 244-259 [doi]

Proof Assistant Decision Procedures for Formalizing OrigamiCezary Kaliszyk, Tetsuo Ida. mkm 2011: 45-57 [doi]

Panda: A Proof Assistant in Natural Deduction for All. A Gentzen Style Proof Assistant for Undergraduate StudentsOlivier Gasquet, François Schwarzentruber, Martin Strecker. ticttl 2011: 85-92 [doi]

Structural Analysis of Narratives with the Coq Proof AssistantAnne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza. itp 2011: 55-70 [doi]

Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System FrameworkGabriel Dos Reis, David Matthews, Yue Li. mkm 2011: 15-29 [doi]

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

Modelling Differential Structures in Proof Assistants: The Graded CaseJesÃºs Aransay, CÃ©sar DomÃnguez. eurocast 2009: 203-210 [doi]

The Twelf Proof AssistantCarsten SchÃ¼rmann. tphol 2009: 79-83 [doi]

Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant SystemsJÃ³nathan Heras, Vico Pascual, Julio Rubio. mkm 2009: 467-473 [doi]

Lambda, the ultimate TA: using a proof assistant to teach programming language foundationsBenjamin C. Pierce. ICFP 2009: 121-122 [doi]

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

Galculator : functional prototype of a Galois-connection based proof assistantPaulo F. Silva, José Nuno Oliveira. ppdp 2008: 44-55 [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.

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

Web Interfaces for Proof AssistantsENTCS, 174(2):49-61, 2007. [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]

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

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

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

Crafting a Proof AssistantAndrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. TYPES 2007: 18-32 [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]

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]

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

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

Towards formalising AADL in Proof AssistantsJean-Paul Bodeveix, David Chemouil, Mamoun Filali, Martin Strecker. ENTCS, 141(3):153-169, 2005. [doi]

A Proof-Centric approach to Mathematical AssistantsLucas Dixon, J. D. Fleuriot. Journal of Applied Logic: Towards Computer Aided Mathematics Systems, 4(4), 2005.

Types with semantics: soundness proof assistantOlha Shkaravska. ICFP 2005: 50-57 [doi]

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

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

Observational Equivalence and Program Extraction in the Coq Proof AssistantNicolas Oury. tlca 2003: 271-285 [doi]

From Proof-Assistants to Distributed Libraries of Mathematics: Tips and PitfallsClaudio Sacerdoti Coen. mkm 2003: 30-44 [doi]

Extracting a formally verified, fully executable compiler from a proof assistantStefan Berghofer, Martin Strecker. ENTCS, 82(2):377-394, 2003. [doi]

Introduction to PAF!, a Proof Assistant for ML Programs VerificationSylvain Baro. TYPES 2004: 51-65 [doi]

A Proof Assistant for Mobile ProcessesXutao Du, Zhoujun Li. appt 2003: 204-214 [doi]

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

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

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.

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.

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]

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

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

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

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

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

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

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

runs on WebDSL