news

30 years of research and development around Coq

Authors:

Gérard Huet,

Hugo HerbelinAuthors Info & Claims

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Page 249

https://doi.org/10.1145/2535838.2537848

Published: 08 January 2014 Publication History

Get Access

Abstract

No abstract available.

Supplementary Material

MP4 File (d2_left_t2.mp4)

Download
282.50 MB

Cited By

View all

de Boer FHiep Hde Gouw S(2023)The Logic of Separation Logic: Models and ProofsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_22(407-426)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_22
Bhurke AKazi F(2021)Methods of Formal Analysis for ICS Protocols and HART - IP CPN modelling2021 Asian Conference on Innovation in Technology (ASIANCON)10.1109/ASIANCON51346.2021.9544603(1-7)Online publication date: 27-Aug-2021
https://doi.org/10.1109/ASIANCON51346.2021.9544603
Wang QKaliszyk C(2021)JEFL: Joint Embedding of Formal Proof LibrariesFrontiers of Combining Systems10.1007/978-3-030-86205-3_9(154-170)Online publication date: 1-Sep-2021
https://doi.org/10.1007/978-3-030-86205-3_9
Show More Cited By

Index Terms

30 years of research and development around Coq

Recommendations

30 years of research and development around Coq
POPL '14
Hammer for Coq: Automation for Dependent Type Theory

Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive Constructions, ...
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 2014

702 pages

ISBN:9781450325448

DOI:10.1145/2535838

General Chair:
Suresh Jagannathan
Purdue University, USA
,
Program Chair:
Peter Sewell
University of Cambridge, UK

ACM SIGPLAN Notices Volume 49, Issue 1
POPL '14
January 2014
661 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2578855
Editor:
Mark W. Bailey
Hamilton College, Clinton, NY
Issue’s Table of Contents

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2014

Check for updates

Author Tags

Qualifiers

News

Conference

POPL '14

Sponsor:

SIGPLAN

POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 22 - 24, 2014

California, San Diego, USA

Acceptance Rates

POPL '14 Paper Acceptance Rate 51 of 220 submissions, 23%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
363
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

de Boer FHiep Hde Gouw S(2023)The Logic of Separation Logic: Models and ProofsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_22(407-426)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_22
Bhurke AKazi F(2021)Methods of Formal Analysis for ICS Protocols and HART - IP CPN modelling2021 Asian Conference on Innovation in Technology (ASIANCON)10.1109/ASIANCON51346.2021.9544603(1-7)Online publication date: 27-Aug-2021
https://doi.org/10.1109/ASIANCON51346.2021.9544603
Wang QKaliszyk C(2021)JEFL: Joint Embedding of Formal Proof LibrariesFrontiers of Combining Systems10.1007/978-3-030-86205-3_9(154-170)Online publication date: 1-Sep-2021
https://doi.org/10.1007/978-3-030-86205-3_9
Marić F(2019)Fast Formal Proof of the Erd?s---Szekeres Conjecture for Convex Polygons with at Most 6 PointsJournal of Automated Reasoning10.1007/s10817-017-9423-762:3(301-329)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s10817-017-9423-7
Keller C(2019)SMTCoq: Mixing Automatic and Interactive Proof TechnologiesProof Technology in Mathematics Research and Teaching10.1007/978-3-030-28483-1_4(73-90)Online publication date: 2-Oct-2019
https://doi.org/10.1007/978-3-030-28483-1_4
Matache CGomes VMulligan D(2017)Programming and Proving with Classical TypesProgramming Languages and Systems10.1007/978-3-319-71237-6_11(215-234)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-71237-6_11
Gauthier TKaliszyk C(2015)Sharing HOL4 and HOL Light Proof KnowledgeProceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Volume 945010.1007/978-3-662-48899-7_26(372-386)Online publication date: 24-Nov-2015
https://dl.acm.org/doi/10.1007/978-3-662-48899-7_26

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations