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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: TASE 2009, Third IEEE International Symposium on Theoretical Aspects of Software Engineering, 29-31 July 2009, Tianjin, China, pp. 233-240, 2009, IEEE Computer Society, 978-0-7695-3757-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
11 | Sylvie Boldo, Guillaume Melquiond |
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 57(4), pp. 462-471, 2008. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 40(1), pp. 61-85, 2008. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, pp. 621-635, 2008, Springer, 978-3-540-89438-4. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca |
Canonical Big Operators. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 86-101, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Matthieu Sozeau, Nicolas Oury |
First-Class Type Classes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 278-293, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks 0001, Iulian Neamtiu |
Formalizing Soundness of Contextual Effects. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 262-277, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Mike Gordon |
Twenty Years of Theorem Proving for HOLs Past, Present and Future. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 1-5, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MPC ![In: Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings, pp. 220-242, 2008, Springer, 978-3-540-70593-2. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Noam Zeilberger |
Focusing and higher-order abstract syntax. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pp. 359-369, 2008, ACM, 978-1-59593-689-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FoSSaCS ![In: Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, pp. 365-379, 2008, Springer, 978-3-540-78497-5. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli |
Oracle Semantics for Concurrent Separation Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESOP ![In: Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, pp. 353-367, 2008, Springer, 978-3-540-78738-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers, pp. 49-63, 2008, Springer, 978-3-642-02443-6. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
mobile devices, Access control models, formal proofs |
11 | Erik Ernst |
First-Class Object Sets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers, pp. 83-99, 2008, Springer, 978-3-642-02443-6. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Object sets, multi-object method calls, composition, types |
11 | Cezary Kaliszyk, Freek Wiedijk |
Merging Procedural and Declarative Proof. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers, pp. 203-219, 2008, Springer, 978-3-642-02443-6. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Laura Effinger-Dean, Matthew Kehrt, Dan Grossman |
Transactional events for ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pp. 103-114, 2008, ACM, 978-1-59593-919-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
synchronous message passing, transactional events, concurrency |
11 | Guillaume Melquiond |
Proving Bounds on Real-Valued Functions with Computations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, pp. 2-17, 2008, Springer, 978-3-540-71069-1. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Rawle C. S. Prince, Neil Ghani, Conor McBride |
Proving Properties about Lists Using Containers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLOPS ![In: Functional and Logic Programming, 9th International Symposium, FLOPS 2008, Ise, Japan, April 14-16, 2008. Proceedings, pp. 97-112, 2008, Springer, 978-3-540-78968-0. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Nicolas Julien |
Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLOPS ![In: Functional and Logic Programming, 9th International Symposium, FLOPS 2008, Ise, Japan, April 14-16, 2008. Proceedings, pp. 48-63, 2008, Springer, 978-3-540-78968-0. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | David Nowak |
On Formal Verification of Arithmetic-Based Cryptographic Primitives. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICISC ![In: Information Security and Cryptology - ICISC 2008, 11th International Conference, Seoul, Korea, December 3-5, 2008, Revised Selected Papers, pp. 368-382, 2008, Springer, 978-3-642-00729-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 15-17, 2008, Valencia, Spain, pp. 44-55, 2008, ACM, 978-1-60558-117-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMOODS ![In: Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings, pp. 132-149, 2008, Springer, 978-3-540-68862-4. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Adam Koprowski, Johannes Waldmann |
Arctic Termination ...Below Zero. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, pp. 202-216, 2008, Springer, 978-3-540-70588-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFIP TCS ![In: Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy, pp. 349-365, 2008, Springer, 978-0-387-09679-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Adam Koprowski, Hans Zantema |
Certification of Proving Termination of Term Rewriting by Matrix Interpretations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SOFSEM ![In: SOFSEM 2008: Theory and Practice of Computer Science, 34th Conference on Current Trends in Theory and Practice of Computer Science, Nový Smokovec, Slovakia, January 19-25, 2008, Proceedings, pp. 328-339, 2008, Springer, 978-3-540-77565-2. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Frédéric Gava, Jean Fortin |
Formal Semantics of a Subset of the Paderborn's BSPlib. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PDCAT ![In: Ninth International Conference on Parallel and Distributed Computing, Applications and Technologies, PDCAT 2008, Dunedin, Otago, New Zealand, 1-4 December 2008, pp. 269-276, 2008, IEEE Computer Society, 978-0-7695-3443-5. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
11 | Chunxiao Lin, Yiyun Chen, Long Li, Bei Hua |
Garbage Collector Verification for Proof-Carrying Code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. Sci. Technol. ![In: J. Comput. Sci. Technol. 22(3), pp. 426-437, 2007. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 39(1), pp. 1-47, 2007. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 19(2), pp. 191-203, 2007. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TGC ![In: Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, pp. 23-40, 2007, Springer, 978-3-540-78662-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Éric Jaeger, Catherine Dubois |
Why Would You Trust B ? ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, pp. 288-302, 2007, Springer, 978-3-540-75558-6. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Prover, Deep embedding, Formal Methods, Confidence |
11 | Zaynah Dargaye, Xavier Leroy |
Mechanized Verification of CPS Transformations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, pp. 211-225, 2007, Springer, 978-3-540-75558-6. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Seth Fogarty, Emir Pasalic, Jeremy G. Siek, Walid Taha |
Concoqtion: indexed types now! ![Search on Bibsonomy](Pics/bibsonomy.png) |
PEPM ![In: Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2007, Nice, France, January 15-16, 2007, pp. 112-121, 2007, ACM, 978-1-59593-620-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Zhaozhong Ni, Dachuan Yu, Zhong Shao |
Using XCAP to Certify Realistic Systems Code: Machine Context Management. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 189-206, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | François Garillot, Benjamin Werner |
Simple Types in Type Theory: Deep and Shallow Encodings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 368-382, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Laurent Théry, Guillaume Hanrot |
Primality Proving with Elliptic Curves. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 319-333, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | David Delahaye, Catherine Dubois, Jean-Frédéric Étienne |
Extracting Purely Functional Contents from Logical Inductive Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 70-85, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry |
A Modular Formalisation of Finite Group Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 86-101, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Andrew W. Appel, Sandrine Blazy |
Separation Logic for Small-Step cminor. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 5-21, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Christoph Benzmüller, Dominik Dietrich, Marvin R. G. Schiller, Serge Autexier |
Deep Inference for Automated Proof Tutoring? ![Search on Bibsonomy](Pics/bibsonomy.png) |
KI ![In: KI 2007: Advances in Artificial Intelligence, 30th Annual German Conference on AI, KI 2007, Osnabrück, Germany, September 10-13, 2007, Proceedings, pp. 435-439, 2007, Springer, 978-3-540-74564-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pp. 109-122, 2007, ACM, 1-59593-575-4. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
impredicative polymorphism, mutable references, recursive types, Kripke models |
11 | Evelyne Contejean |
Modeling Permutations in Coqfor Coccinelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Rewriting, Computation and Proof ![In: Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, pp. 259-269, 2007, Springer, 978-3-540-73146-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Gilles Barthe, David Pichardie, Tamara Rezk |
A Certified Lightweight Non-interference Java Bytecode Verifier. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESOP ![In: Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings, pp. 125-140, 2007, Springer, 978-3-540-71314-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Robert Atkey |
CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers, pp. 18-32, 2007, Springer, 978-3-540-68084-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pp. 1-12, 2007, ACM, 978-1-59593-815-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Sylvain Conchon, Jean-Christophe Filliâtre |
A persistent union-find data structure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ML ![In: Proceedings of the ACM Workshop on ML, 2007, Freiburg, Germany, October 5, 2007, pp. 37-46, 2007, ACM, 978-1-59593-676-9. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
formal verification, persistence, union-find |
11 | Adam Chlipala |
A certified type-preserving compiler from lambda calculus to assembly language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007, pp. 54-65, 2007, ACM, 978-1-59593-633-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007, pp. 468-479, 2007, ACM, 978-1-59593-633-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007, pp. 66-77, 2007, ACM, 978-1-59593-633-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLDI ![In: Proceedings of TLDI'07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Nice, France, January 16, 2007, pp. 67-78, 2007, ACM, 1-59593-393-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 14-16, 2007, Wroclaw, Poland, pp. 1-12, 2007, ACM, 978-1-59593-769-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAST ![In: Computer Aided Systems Theory - EUROCAST 2007, 11th International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 12-16, 2007, Revised Selected Papers, pp. 233-240, 2007, Springer, 978-3-540-75866-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Reynald Affeldt, Miki Tanaka, Nicolas Marti |
Formal Proof of Provable Security by Game-Playing in a Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ProvSec ![In: Provable Security, First International Conference, ProvSec 2007, Wollongong, Australia, November 1-2, 2007, Proceedings, pp. 151-168, 2007, Springer, 978-3-540-75669-9. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Robert L. Constable, Wojciech Moczydlowski |
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFCS ![In: Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings, pp. 147-161, 2007, Springer, 978-3-540-72732-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain |
Certification of Automated Termination Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FroCoS ![In: Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007, Liverpool, UK, September 10-12, 2007, Proceedings, pp. 148-162, 2007, Springer, 978-3-540-74620-1. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo |
Foundational Typed Assembly Language with Certified Garbage Collection. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007, June 5-8, 2007, Shanghai, China, pp. 326-338, 2007, IEEE Computer Society, 0-7695-2856-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | David Nowak |
A Framework for Game-Based Security Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICICS ![In: Information and Communications Security, 9th International Conference, ICICS 2007, Zhengzhou, China, December 12-15, 2007, Proceedings, pp. 319-333, 2007, Springer, 978-3-540-77047-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
security, game, formal verification, proof assistant |
11 | Pierre Corbineau, Cezary Kaliszyk |
Cooperative Repositories for Formal Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings, pp. 221-234, 2007, Springer, 978-3-540-73083-5. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Solange Coupet-Grimal, William Delobel |
An effective proof of the well-foundedness of the multiset path ordering. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Algebra Eng. Commun. Comput. ![In: Appl. Algebra Eng. Commun. Comput. 17(6), pp. 453-469, 2006. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Stud Logica ![In: Stud Logica 82(1), pp. 25-49, 2006. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 36(3), pp. 259-285, 2006. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006. Revised Papers, pp. 139-156, 2006, Springer, 978-3-540-77355-9. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Sandrine-Dominique Gouraud, Arnaud Gotlieb |
Using CHRs to Generate Functional Test Cases for the Java Card Virtual Machine. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PADL ![In: Practical Aspects of Declarative Languages, 8th International Symposium, PADL 2006, Charleston, SC, USA, January 9-10, 2006, Proceedings, pp. 1-15, 2006, Springer, 3-540-30947-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006, Proceedings, pp. 400-419, 2006, Springer, 3-540-47460-9. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Sylvie Boldo, César A. Muñoz |
Provably faithful evaluation of polynomials. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), Dijon, France, April 23-27, 2006, pp. 1328-1332, 2006, ACM, 1-59593-108-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), Dijon, France, April 23-27, 2006, pp. 1318-1322, 2006, ACM, 1-59593-108-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Zhaozhong Ni, Zhong Shao |
Certified assembly programming with embedded code pointers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, pp. 320-333, 2006, ACM, 1-59593-027-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, pp. 78-92, 2006, Springer, 978-3-540-74463-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli |
Crafting a Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, pp. 18-32, 2006, Springer, 978-3-540-74463-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Frédéric Besson |
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, pp. 48-62, 2006, Springer, 978-3-540-74463-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Frédéric Loulergue |
A calculus of functional BSP programs with projection. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IPDPS ![In: 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), Proceedings, 25-29 April 2006, Rhodes Island, Greece, 2006, IEEE. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 423-437, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Assia Mahboubi |
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 438-452, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Roland Zumkeller |
Formal Global Optimisation with Taylor Models. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 408-422, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz |
Consistency and Completeness of Rewriting in the Calculus of Constructions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 619-631, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 11-14, 2006, pp. 401-414, 2006, ACM, 1-59593-320-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASIAN ![In: Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Revised Selected Papers, pp. 346-360, 2006, Springer, 978-3-540-77504-1. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Devrim Unal, M. Ufuk Çaglayan |
Theorem proving for modeling and conflict checking of authorization policies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISCN ![In: Proceedings of the International Symposium on Computer Networks, ISCN 2006, June 16-18, 2006, Istanbul, Turkey, pp. 146-151, 2006, IEEE. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Benjamin Grégoire, Laurent Théry, Benjamin Werner |
A Computational Approach to Pocklington Certificates in Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLOPS ![In: Functional and Logic Programming, 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings, pp. 97-113, 2006, Springer, 3-540-33438-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VMCAI ![In: Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, pp. 174-189, 2006, Springer, 3-540-31139-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Sen Xiang, Yiyun Chen, Chunxiao Lin, Long Li |
Modularly Certified Dynamic Storage Allocation in SCAP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
QSIC ![In: Sixth International Conference on Quality Software (QSIC 2006), 26-28 October 2006, Beijing, China, pp. 321-328, 2006, IEEE Computer Society, 0-7695-2718-3. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Nick Benton |
Abstracting Allocation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, pp. 182-196, 2006, Springer, 3-540-45458-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects in Security and Trust ![In: Formal Aspects in Security and Trust, Fourth International Workshop, FAST 2006, Hamilton, Ontario, Canada, August 26-27, 2006, Revised Selected Papers, pp. 220-234, 2006, Springer, 978-3-540-75226-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
11 | Marc Bezem, Thierry Coquand |
Automating Coherent Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, pp. 246-260, 2005, Springer, 3-540-30553-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLCA ![In: Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, pp. 278-292, 2005, Springer, 3-540-25593-1. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
11 | David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider |
Certified Memory Usage Analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings, pp. 91-106, 2005, Springer, 3-540-27882-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Processes, Terms and Cycles ![In: Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, pp. 224-250, 2005, Springer, 3-540-30911-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Guillaume Dufay, Amy P. Felty, Stan Matwin |
Privacy-Sensitive Information Flow with JML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pp. 116-130, 2005, Springer, 3-540-28005-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAST ![In: Computer Aided Systems Theory - EUROCAST 2005, 10th International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 7-11, 2005, Revised Selected Papers, pp. 69-80, 2005, Springer, 3-540-29002-8. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Sabrina Tarento |
Machine-Checked Security Proofs of Cryptographic Signature Schemes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESORICS ![In: Computer Security - ESORICS 2005, 10th European Symposium on Research in Computer Security, Milan, Italy, September 12-14, 2005, Proceedings, pp. 140-158, 2005, Springer, 3-540-28963-1. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Sylvie Boldo, Marc Daumas |
Properties of two's complement floating point notations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 5(2-3), pp. 237-246, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Digital signal processing, Avionics, Formal proof |
11 | Solange Coupet-Grimal, Line Jakubiec |
Certifying circuits in Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 16(4), pp. 352-373, 2004. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, pp. 50-65, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Pietro Di Gianantonio, Marino Miculan |
Unifying Recursive and Co-recursive Definitions in Sheaf Categories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FoSSaCS ![In: Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, pp. 136-150, 2004, Springer, 3-540-21298-1. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Solange Coupet-Grimal, William Delobel |
A Uniform and Certified Approach for Two Static Analyses. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 115-137, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Robin Adams 0001 |
Formalized Metatheory with Terms Represented by an Indexed Family of Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 1-16, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli |
A Content Based Mathematical Search Engine: Whelp. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 17-32, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Claudio Sacerdoti Coen |
A Semi-reflexive Tactic for (Sub-)Equational Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 98-114, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
11 | Gilles Barthe, Sabrina Tarento |
A Machine-Checked Formalization of the Random Oracle Model. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 33-49, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, pp. 385-399, 2004, Springer, 3-540-22345-2. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|