Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions | Guide books | ACM Digital Library (2024)

Ishibashi T and Ogata K Formal Specification and Model Checking of Raft Leader Election in Maude* Proceedings of the 2023 12th International Conference on Software and Computer Applications, (41-45)

Al-Odat Z, Khan S and Al-Qtiemat E (2023). A modified secure hash design to circumvent collision and length extension attacks, Journal of Information Security and Applications, 71:C, Online publication date: 1-Dec-2022.

Zaheri M Towards consistency management in low-code platforms Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, (176-181)

Da Silveira A, Ribeiro R, Nunes M, Torrens P and Roggia K A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq Proceedings of the XXVI Brazilian Symposium on Programming Languages, (1-7)

Wang Q, Wong Y, Que Z and Luk W Verifying Hardware Optimizations for Efficient Acceleration Proceedings of the 12th International Symposium on Highly-Efficient Accelerators and Reconfigurable Technologies, (17-23)

Xiao L and Zhu H (2022). UTP semantics for the MCA ARMv8 architecture, Journal of Systems Architecture: the EUROMICRO Journal, 125:C, Online publication date: 1-Apr-2022.

Schultz W, Dardik I and Tripakis S Formal verification of a distributed dynamic reconfiguration protocol Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, (143-152)

Yuan S and Talpin J Verified functional programming of an IoT operating system's bootloader Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, (89-97)

Henz M, Tan T, Chua Z, Jung P, Tan Y, Zhang X and Zhao J A stepper for a functional JavaScript sublanguage Proceedings of the 2021 ACM SIGPLAN International Symposium on SPLASH-E, (71-81)

Dupont G, Ait-Ameur Y, Singh N and Pantel M (2021). Event-B Hybridation, ACM Transactions on Embedded Computing Systems, 20:4, (1-37), Online publication date: 31-Jul-2021.

Zhang Q, Qiao J, Meng Q and Chen Y (2020). Automatic kernel code synthesis and verification, Computers and Security, 91:C, Online publication date: 1-Apr-2020.

Bana G, Chadha R, Eeralla A and Okada M (2019). Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability, ACM Transactions on Computational Logic, 21:1, (1-44), Online publication date: 10-Jan-2020.

Abadi M and Plotkin G (2019). A simple differentiable programming language, Proceedings of the ACM on Programming Languages, 4:POPL, (1-28), Online publication date: 1-Jan-2020.

Handley M, Vazou N and Hutton G (2019). Liquidate your assets: reasoning about resource usage in liquid Haskell, Proceedings of the ACM on Programming Languages, 4:POPL, (1-27), Online publication date: 1-Jan-2020.

Cohen L, Abreu Faro S and Tate R (2019). The Effects of Effects on Constructivism, Electronic Notes in Theoretical Computer Science (ENTCS), 347:C, (87-120), Online publication date: 30-Nov-2019.

Celik A, Palmskog K, Parovic M, Arias E and Gligoric M Mutation analysis for Coq Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, (539-551)

Vukotic I, Rahli V and Esteves-Veríssimo P (2019). Asphalion: trustworthy shielding against Byzantine faults, Proceedings of the ACM on Programming Languages, 3:OOPSLA, (1-32), Online publication date: 10-Oct-2019.

Konnov I, Kukovec J and Tran T (2019). TLA+ model checking made symbolic, Proceedings of the ACM on Programming Languages, 3:OOPSLA, (1-30), Online publication date: 10-Oct-2019.

Rodrigues V, Donetti S and Damiani F (2019). Certifying delta-oriented programs, Software and Systems Modeling (SoSyM), 18:5, (2875-2906), Online publication date: 1-Oct-2019.

Danvy O Mystery functions Proceedings of the 31st Symposium on Implementation and Application of Functional Languages, (1-9)

Mokhov A, Lukyanov G, Marlow S and Dimino J (2019). Selective applicative functors, Proceedings of the ACM on Programming Languages, 3:ICFP, (1-29), Online publication date: 26-Jul-2019.

Algehed M and Bernardy J (2019). Simple noninterference from parametricity, Proceedings of the ACM on Programming Languages, 3:ICFP, (1-22), Online publication date: 26-Jul-2019.

Eremondi J, Tanter É and Garcia R (2019). Approximate normalization for gradual dependent types, Proceedings of the ACM on Programming Languages, 3:ICFP, (1-30), Online publication date: 26-Jul-2019.

Rahli V, Bickford M, Cohen L and Constable R (2019). Bar Induction is Compatible with Constructive Type Theory, Journal of the ACM, 66:2, (1-35), Online publication date: 26-Apr-2019.

Chen X and Roşu G —A Semantic Framework for Programming Languages and Formal Analysis Engineering Trustworthy Software Systems, (122-158)

Petz A and Alexander P A copland attestation manager Proceedings of the 6th Annual Symposium on Hot Topics in the Science of Security, (1-10)

Lammich P and Sefidgar S (2019). Formalizing Network Flow Algorithms, Journal of Automated Reasoning, 62:2, (261-280), Online publication date: 1-Feb-2019.

Balabonski T, Delga A, Rieg L, Tixeuil S and Urbain X (2019). Synchronous Gathering without Multiplicity Detection, Theory of Computing Systems, 63:2, (200-218), Online publication date: 1-Feb-2019.

Coblenz M, Aldrich J, Myers B and Sunshine J Interdisciplinary programming language design Proceedings of the 2018 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, (133-146)

K. K, Rebeiro C and Hazra A (2018). An Algorithmic Approach to Formally Verify an ECC Library, ACM Transactions on Design Automation of Electronic Systems, 23:5, (1-26), Online publication date: 18-Oct-2018.

Delfino T and Ribeiro R Towards certified virtual machine-based regular expression parsing Proceedings of the XXII Brazilian Symposium on Programming Languages, (67-74)

Benedikt M How Can Reasoners Simplify Database Querying (And Why Haven't They Done It Yet)? Proceedings of the 37th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, (1-15)

Ribeiro R and Bois A Certified Bit-Coded Regular Expression Parsing Proceedings of the 21st Brazilian Symposium on Programming Languages, (1-8)

Cheng Z and Tisi M A Deductive Approach for Fault Localization in ATL Model Transformations Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering - Volume 10202, (300-317)

Schmid G and Kuncak V SMT-based checking of predicate-qualified types for Scala Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala, (31-40)

Mandrykin M and Khoroshilov A (2016). Towards deductive verification of C programs with shared data, Programming and Computing Software, 42:5, (324-332), Online publication date: 1-Sep-2016.

Paulson L Automated theorem proving for special functions Proceedings of the 2014 Symposium on Symbolic-Numeric Computation, (3-8)

Alglave J, Maranget L and Tautschnig M (2014). Herding Cats, ACM Transactions on Programming Languages and Systems, 36:2, (1-74), Online publication date: 1-Jul-2014.

Alama J, Heskes T, Kühlwein D, Tsivtsivadze E and Urban J (2014). Premise Selection for Mathematics by Corpus Analysis and Kernel Methods, Journal of Automated Reasoning, 52:2, (191-213), Online publication date: 1-Feb-2014.

Jedynak W, Biernacka M and Biernacki D An operational foundation for the tactic language of Coq Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, (25-36)

Boldo S, Clément F, Filliâtre J, Mayero M, Melquiond G and Weis P (2013). Wave Equation Numerical Resolution, Journal of Automated Reasoning, 50:4, (423-456), Online publication date: 1-Apr-2013.

Zanarini D, Luna C and Sierra L Alternating-Time temporal logic in the calculus of (co)inductive constructions Proceedings of the 15th Brazilian conference on Formal Methods: foundations and applications, (210-225)

Leino K Automating induction with an SMT solver Proceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation, (315-331)

Achten P, Eekelen M, Koopman P and Morazán M (2010). Trends in Trends in Functional Programming 1999/2000 versus 2007/2008, Higher-Order and Symbolic Computation, 23:4, (465-487), Online publication date: 1-Nov-2010.

Kang E and Jackson D Patterns for building dependable systems with trusted bases Proceedings of the 17th Conference on Pattern Languages of Programs, (1-14)

Dargaye Z and Leroy X Mechanized Verification of CPS Transformations Logic for Programming, Artificial Intelligence, and Reasoning, (211-225)

Pierce B, Sewell P, Weirich S and Zdancewic S It Is Time to Mechanize Programming Language Metatheory Verified Software: Theories, Tools, Experiments, (26-30)

Cui S, Donnelly K and Xi H System description Proceedings of the 5th international conference on Frontiers of Combining Systems, (310-320)

Abel A, Coquand T and Norell U Connecting a logical framework to a first-order logic prover Proceedings of the 5th international conference on Frontiers of Combining Systems, (285-301)

Jorge J, Gulías V, Freire J and Sánchez J Towards a certified and efficient computing of gröbner bases Proceedings of the 10th international conference on Computer Aided Systems Theory, (111-120)

McBride C, Goguen H and McKinna J A few constructions on constructors Proceedings of the 2004 international conference on Types for Proofs and Programs, (186-200)

Mamane L Surreal numbers in coq Proceedings of the 2004 international conference on Types for Proofs and Programs, (170-185)

Danvy O The Tortoise and the Hare Algorithmfor Finite Lists, Compositionally, ACM Transactions on Programming Languages and Systems, 0:0