Search results for "Coq"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
11	Ming Fu, Yu Zhang 0086, Yong Li	Formal Reasoning about Concurrent Assembly Code with Reentrant Locks.	TASE	2009	DBLP DOI BibTeX RDF
11	Sylvie Boldo, Guillaume Melquiond	Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd.	IEEE Trans. Computers	2008	DBLP DOI BibTeX RDF	Verification, Computer arithmetic
11	Marc Bezem, Dimitri Hendriks	On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Coherent logic, Proof objects, Hessenberg’s theorem, Automated theorem proving
11	Ulrich Schöpp	A Formalised Lower Bound on Undirected Graph Reachability.	LPAR	2008	DBLP DOI BibTeX RDF
11	Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca	Canonical Big Operators.	TPHOLs	2008	DBLP DOI BibTeX RDF
11	Matthieu Sozeau, Nicolas Oury	First-Class Type Classes.	TPHOLs	2008	DBLP DOI BibTeX RDF
11	Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks 0001, Iulian Neamtiu	Formalizing Soundness of Contextual Effects.	TPHOLs	2008	DBLP DOI BibTeX RDF
11	Mike Gordon	Twenty Years of Theorem Proving for HOLs Past, Present and Future.	TPHOLs	2008	DBLP DOI BibTeX RDF
11	Ralph Matthes	Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening.	MPC	2008	DBLP DOI BibTeX RDF
11	Noam Zeilberger	Focusing and higher-order abstract syntax.	POPL	2008	DBLP DOI BibTeX RDF	pattern-matching, higher-order abstract syntax, focusing
11	Bruno Barras, Bruno Bernardo	The Implicit Calculus of Constructions as a Programming Language with Dependent Types.	FoSSaCS	2008	DBLP DOI BibTeX RDF
11	Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli	Oracle Semantics for Concurrent Separation Logic.	ESOP	2008	DBLP DOI BibTeX RDF
11	Juan Manuel Crespo, Gustavo Betarte, Carlos Luna 0001	A Framework for the Analysis of Access Control Models for Interactive Mobile Devices.	TYPES	2008	DBLP DOI BibTeX RDF	mobile devices, Access control models, formal proofs
11	Erik Ernst	First-Class Object Sets.	TYPES	2008	DBLP DOI BibTeX RDF	Object sets, multi-object method calls, composition, types
11	Cezary Kaliszyk, Freek Wiedijk	Merging Procedural and Declarative Proof.	TYPES	2008	DBLP DOI BibTeX RDF
11	Laura Effinger-Dean, Matthew Kehrt, Dan Grossman	Transactional events for ML.	ICFP	2008	DBLP DOI BibTeX RDF	synchronous message passing, transactional events, concurrency
11	Guillaume Melquiond	Proving Bounds on Real-Valued Functions with Computations.	IJCAR	2008	DBLP DOI BibTeX RDF
11	Rawle C. S. Prince, Neil Ghani, Conor McBride	Proving Properties about Lists Using Containers.	FLOPS	2008	DBLP DOI BibTeX RDF
11	Nicolas Julien	Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base.	FLOPS	2008	DBLP DOI BibTeX RDF
11	David Nowak	On Formal Verification of Arithmetic-Based Cryptographic Primitives.	ICISC	2008	DBLP DOI BibTeX RDF	machine formalization, CSPRBG, semantic security, cryptographic primitives
11	Paulo F. Silva 0001, José Nuno Oliveira	'Galculator': functional prototype of a Galois-connection based proof assistant.	PPDP	2008	DBLP DOI BibTeX RDF	point-free notation, haskell, DSL, Galois connections, proof assistant, GADT
11	Laurent Hubert, Thomas P. Jensen, David Pichardie	Semantic Foundations and Inference of Non-null Annotations.	FMOODS	2008	DBLP DOI BibTeX RDF
11	Adam Koprowski, Johannes Waldmann	Arctic Termination ...Below Zero.	RTA	2008	DBLP DOI BibTeX RDF
11	Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub	From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures.	IFIP TCS	2008	DBLP DOI BibTeX RDF
11	Adam Koprowski, Hans Zantema	Certification of Proving Termination of Term Rewriting by Matrix Interpretations.	SOFSEM	2008	DBLP DOI BibTeX RDF
11	Frédéric Gava, Jean Fortin	Formal Semantics of a Subset of the Paderborn's BSPlib.	PDCAT	2008	DBLP DOI BibTeX RDF
11	Chunxiao Lin, Yiyun Chen, Long Li, Bei Hua	Garbage Collector Verification for Proof-Carrying Code.	J. Comput. Sci. Technol.	2007	DBLP DOI BibTeX RDF	program safety, program verification, proof-carrying code, garbage collector
11	Alberto Ciaffaglione, Luigi Liquori, Marino Miculan	Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Functional and imperative object-calculi, Logical foundations of programming, Coinductive type theories, Logical frameworks, Interactive theorem proving
11	Bart Jacobs 0001, Sjaak Smetsers, Ronny Wichers Schreur	Code-carrying theories.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Compression, Code generation, Functional languages, Unification, PVS, Proof assistants
11	Benjamin Grégoire, Jorge Luis Sacchini	Combining a Verification Condition Generator for a Bytecode Language with Static Analyses.	TGC	2007	DBLP DOI BibTeX RDF
11	Éric Jaeger, Catherine Dubois	Why Would You Trust B ?	LPAR	2007	DBLP DOI BibTeX RDF	Prover, Deep embedding, Formal Methods, Confidence
11	Zaynah Dargaye, Xavier Leroy	Mechanized Verification of CPS Transformations.	LPAR	2007	DBLP DOI BibTeX RDF
11	Seth Fogarty, Emir Pasalic, Jeremy G. Siek, Walid Taha	Concoqtion: indexed types now!	PEPM	2007	DBLP DOI BibTeX RDF
11	Zhaozhong Ni, Dachuan Yu, Zhong Shao	Using XCAP to Certify Realistic Systems Code: Machine Context Management.	TPHOLs	2007	DBLP DOI BibTeX RDF
11	François Garillot, Benjamin Werner	Simple Types in Type Theory: Deep and Shallow Encodings.	TPHOLs	2007	DBLP DOI BibTeX RDF
11	Laurent Théry, Guillaume Hanrot	Primality Proving with Elliptic Curves.	TPHOLs	2007	DBLP DOI BibTeX RDF
11	David Delahaye, Catherine Dubois, Jean-Frédéric Étienne	Extracting Purely Functional Contents from Logical Inductive Types.	TPHOLs	2007	DBLP DOI BibTeX RDF
11	Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry	A Modular Formalisation of Finite Group Theory.	TPHOLs	2007	DBLP DOI BibTeX RDF
11	Andrew W. Appel, Sandrine Blazy	Separation Logic for Small-Step cminor.	TPHOLs	2007	DBLP DOI BibTeX RDF
11	Christoph Benzmüller, Dominik Dietrich, Marvin R. G. Schiller, Serge Autexier	Deep Inference for Automated Proof Tutoring?	KI	2007	DBLP DOI BibTeX RDF
11	Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, Jérôme Vouillon	A very modal model of a modern, major, general type system.	POPL	2007	DBLP DOI BibTeX RDF	impredicative polymorphism, mutable references, recursive types, Kripke models
11	Evelyne Contejean	Modeling Permutations in Coqfor Coccinelle.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
11	Gilles Barthe, David Pichardie, Tamara Rezk	A Certified Lightweight Non-interference Java Bytecode Verifier.	ESOP	2007	DBLP DOI BibTeX RDF
11	Robert Atkey	CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types.	TYPES	2007	DBLP DOI BibTeX RDF
11	Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa	Ott: effective tool support for the working semanticist.	ICFP	2007	DBLP DOI BibTeX RDF
11	Sylvain Conchon, Jean-Christophe Filliâtre	A persistent union-find data structure.	ML	2007	DBLP DOI BibTeX RDF	formal verification, persistence, union-find
11	Adam Chlipala	A certified type-preserving compiler from lambda calculus to assembly language.	PLDI	2007	DBLP DOI BibTeX RDF	denotational semantics, dependent types, compiler verification, interactive proof assistants
11	Andrew McCreight, Zhong Shao, Chunxiao Lin, Long Li	A general framework for certifying garbage collectors and their mutators.	PLDI	2007	DBLP DOI BibTeX RDF	assembly code verification, garbage collection, abstract data type, separation logic, proof-carrying code
11	Hongxu Cai, Zhong Shao, Alexander Vaynberg	Certified self-modifying code.	PLDI	2007	DBLP DOI BibTeX RDF	assembly code verification, runtime code manipulation, self-modifying code, hoare logic, modular verification
11	Xinyu Feng 0001, Zhaozhong Ni, Zhong Shao, Yu Guo	An open framework for foundational proof-carrying code.	TLDI	2007	DBLP DOI BibTeX RDF	foundational proof-carrying code, open framework, interoperability, modularity, program verification
11	Nick Benton, Uri Zarfaty	Formalizing and verifying semantic type soundness of a simple compiler.	PPDP	2007	DBLP DOI BibTeX RDF	relational para-metricity, separation logic, proof assistants, compiler verification, type soundness
11	J. Santiago Jorge, Víctor M. Gulías, Laura M. Castro	Verification of Program Properties Using Different Theorem Provers: A Case Study.	EUROCAST	2007	DBLP DOI BibTeX RDF
11	Reynald Affeldt, Miki Tanaka, Nicolas Marti	Formal Proof of Provable Security by Game-Playing in a Proof Assistant.	ProvSec	2007	DBLP DOI BibTeX RDF
11	Robert L. Constable, Wojciech Moczydlowski	Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus.	LFCS	2007	DBLP DOI BibTeX RDF
11	Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain	Certification of Automated Termination Proofs.	FroCoS	2007	DBLP DOI BibTeX RDF
11	Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo	Foundational Typed Assembly Language with Certified Garbage Collection.	TASE	2007	DBLP DOI BibTeX RDF
11	David Nowak	A Framework for Game-Based Security Proofs.	ICICS	2007	DBLP DOI BibTeX RDF	security, game, formal verification, proof assistant
11	Pierre Corbineau, Cezary Kaliszyk	Cooperative Repositories for Formal Proofs.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
11	Solange Coupet-Grimal, William Delobel	An effective proof of the well-foundedness of the multiset path ordering.	Appl. Algebra Eng. Commun. Comput.	2006	DBLP DOI BibTeX RDF	Well-foundedness, Multiset path order, Termination, Constructive logic
11	Ulrich Berger 0001, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg	Program Extraction from Normalization Proofs.	Stud Logica	2006	DBLP DOI BibTeX RDF	Normalization by evaluation, program extraction from proofs, realizability, typed lambda calculus
11	Carlos Simpson	Explaining Gabriel-Zisman Localization to the Computer.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	calculus of fractions, computer proof verification, localization, category, proof assistant, functor
11	Julien Narboux	Mechanical Theorem Proving in Tarski's Geometry.	Automated Deduction in Geometry	2006	DBLP DOI BibTeX RDF
11	Sandrine-Dominique Gouraud, Arnaud Gotlieb	Using CHRs to Generate Functional Test Cases for the Java Card Virtual Machine.	PADL	2006	DBLP DOI BibTeX RDF	CHR, Java Card Virtual Machine, Software testing
11	Nicolas Marti, Reynald Affeldt, Akinori Yonezawa	Formal Verification of the Heap Manager of an Operating System Using Separation Logic.	ICFEM	2006	DBLP DOI BibTeX RDF
11	Sylvie Boldo, César A. Muñoz	Provably faithful evaluation of polynomials.	SAC	2006	DBLP DOI BibTeX RDF	formal verification, floating-point, polynomial evaluation
11	Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond	Assisted verification of elementary functions using Gappa.	SAC	2006	DBLP DOI BibTeX RDF
11	Zhaozhong Ni, Zhong Shao	Certified assembly programming with embedded code pointers.	POPL	2006	DBLP DOI BibTeX RDF	embedded code pointers, hoare logic, proof-carrying code, higher-order functions
11	Pierre Corbineau	Deciding Equality in the Constructor Theory.	TYPES	2006	DBLP DOI BibTeX RDF
11	Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli	Crafting a Proof Assistant.	TYPES	2006	DBLP DOI BibTeX RDF
11	Frédéric Besson	Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.	TYPES	2006	DBLP DOI BibTeX RDF
11	Frédéric Loulergue	A calculus of functional BSP programs with projection.	IPDPS	2006	DBLP DOI BibTeX RDF
11	Benjamin Grégoire, Laurent Théry	A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers.	IJCAR	2006	DBLP DOI BibTeX RDF
11	Assia Mahboubi	Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials.	IJCAR	2006	DBLP DOI BibTeX RDF
11	Roland Zumkeller	Formal Global Optimisation with Taylor Models.	IJCAR	2006	DBLP DOI BibTeX RDF
11	Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz	Consistency and Completeness of Rewriting in the Calculus of Constructions.	IJCAR	2006	DBLP DOI BibTeX RDF
11	Xinyu Feng 0001, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni	Modular verification of assembly code with stack-based control abstractions.	PLDI	2006	DBLP DOI BibTeX RDF	assembly code verification, control abstractions, stack-based, modularity, proof-carrying code
11	Reynald Affeldt, Nicolas Marti	An Approach to Formal Verification of Arithmetic Functions in Assembly.	ASIAN	2006	DBLP DOI BibTeX RDF
11	Devrim Unal, M. Ufuk Çaglayan	Theorem proving for modeling and conflict checking of authorization policies.	ISCN	2006	DBLP DOI BibTeX RDF
11	Benjamin Grégoire, Laurent Théry, Benjamin Werner	A Computational Approach to Pocklington Certificates in Type Theory.	FLOPS	2006	DBLP DOI BibTeX RDF
11	Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula	A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety.	VMCAI	2006	DBLP DOI BibTeX RDF
11	Sen Xiang, Yiyun Chen, Chunxiao Lin, Long Li	Modularly Certified Dynamic Storage Allocation in SCAP.	QSIC	2006	DBLP DOI BibTeX RDF
11	Nick Benton	Abstracting Allocation.	CSL	2006	DBLP DOI BibTeX RDF
11	Santiago Zanella Béguelin, Gustavo Betarte, Carlos Luna 0001	A Formal Specification of the MIDP 2.0 Security Model.	Formal Aspects in Security and Trust	2006	DBLP DOI BibTeX RDF
11	Marc Bezem, Thierry Coquand	Automating Coherent Logic.	LPAR	2005	DBLP DOI BibTeX RDF
11	Stan Matwin, Amy P. Felty, István T. Hernádvölgyi, Venanzio Capretta	Privacy in Data Mining Using Formal Methods.	TLCA	2005	DBLP DOI BibTeX RDF
11	David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider	Certified Memory Usage Analysis.	FM	2005	DBLP DOI BibTeX RDF	certified memory analysis, Program analysis, theorem proving, constraint solving
11	Jean-Pierre Jouannaud	Higher-Order Rewriting: Framework, Confluence and Termination.	Processes, Terms and Cycles	2005	DBLP DOI BibTeX RDF
11	Guillaume Dufay, Amy P. Felty, Stan Matwin	Privacy-Sensitive Information Flow with JML.	CADE	2005	DBLP DOI BibTeX RDF
11	José Luis Freire, Enrique Freire Brañas, Antonio Blanco	On Recursive Functions and Well-Founded Relations in the Calculus of Constructions.	EUROCAST	2005	DBLP DOI BibTeX RDF
11	Sabrina Tarento	Machine-Checked Security Proofs of Cryptographic Signature Schemes.	ESORICS	2005	DBLP DOI BibTeX RDF
11	Sylvie Boldo, Marc Daumas	Properties of two's complement floating point notations.	Int. J. Softw. Tools Technol. Transf.	2004	DBLP DOI BibTeX RDF	Digital signal processing, Avionics, Formal proof
11	Solange Coupet-Grimal, Line Jakubiec	Certifying circuits in Type Theory.	Formal Aspects Comput.	2004	DBLP DOI BibTeX RDF	Co-induction, Formal methods, Type theory, Dependent types, Extraction, Hardware verification
11	Olivier Boite	Proof Reuse with Extended Inductive Types.	TPHOLs	2004	DBLP DOI BibTeX RDF
11	Pietro Di Gianantonio, Marino Miculan	Unifying Recursive and Co-recursive Definitions in Sheaf Categories.	FoSSaCS	2004	DBLP DOI BibTeX RDF
11	Solange Coupet-Grimal, William Delobel	A Uniform and Certified Approach for Two Static Analyses.	TYPES	2004	DBLP DOI BibTeX RDF
11	Robin Adams 0001	Formalized Metatheory with Terms Represented by an Indexed Family of Types.	TYPES	2004	DBLP DOI BibTeX RDF
11	Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli	A Content Based Mathematical Search Engine: Whelp.	TYPES	2004	DBLP DOI BibTeX RDF
11	Claudio Sacerdoti Coen	A Semi-reflexive Tactic for (Sub-)Equational Reasoning.	TYPES	2004	DBLP DOI BibTeX RDF
11	Gilles Barthe, Sabrina Tarento	A Machine-Checked Formalization of the Random Oracle Model.	TYPES	2004	DBLP DOI BibTeX RDF
11	Gilles Barthe, Jan Cederquist, Sabrina Tarento	A Machine-Checked Formalization of the Generic Model and the Random Oracle Model.	IJCAR	2004	DBLP DOI BibTeX RDF