2005
|
|
Enabling Large Scale Coherency Among Mathematical Texts By Stuart F. Allen and Robert L. Constable. Submitted to JoDI, 2005.
|
|
2004
|
|
|
Abstract Identifiers, Intertextual
Reference and a Computational Basis for Recordkeeping
By S. F. Allen. In First Monday, volume 9, number 2, 2004.
|
|
2003
|
|
|
Constructively Characterizing Fold and Unfold
By T. Weber and J. Caldwell. In 13th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR), 2003.
|
|
|
|
Dependent Intersection: A New Way of Defining Records in Type Theory
By A. Kopylov. In Proceedings of LICS 18, IEEE, 2003.
|
|
|
|
The FDL Navigator: Browsing and Manipulating Formal Content
By C. Kreitz. Technical Report, Cornell University, 2003.
|
|
|
|
Formal Compiler Implementation in a Logical Framework.
By J. Hickey, et al. Technical Report, California Institute of Technology, 2003.
|
|
|
|
Formalizing Abstract Algebra in Type Theory with Dependent Records
By X. Yu, et al. Accepted to TPHOLs 2003 "Track B." |
|
|
|
Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant
By Y. Bryukhov, et al. Accepted to TPHOLs
2003 "Track B."
|
|
|
|
Information-Intensive Proof Technology
By R. Constable. Lecture Notes for the Marktoberdorf NATO Summer School, 2003.
|
|
|
|
Introduction to the Objective Caml Programming Language
By J. Hickey. California Institute of Technology, 2003.
|
|
|
|
A Logic of Events
By M. Bickford and R. Constable. Technical Report, Cornell University, 2003.
|
|
|
|
MetaPRL - A Modular Logical Environment
By J. Hickey, et al. In Proceedings of TPHOLS, 2003.
|
|
|
|
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics
By S. Allen, et al. Technical Report, Cornell University, 2003.
|
|
2002
|
|
|
Abstract Identifiers and Textual Reference
By S. Allen. Technical Report, Cornell University, 2002.
|
|
|
|
Computational Complexity and Induction for Partial Computable
Functions in Type Theory
By R. Constable and K. Crary. Essays in Honor of Solomon Feferman, 2002.
|
|
|
|
Formal Design Environments
By B. Aydemir, A. Granicz, and J. Hickey. TPHOLs, 2002.
Appears in NASA Technical Report NASA/CP-2002-211736, 2002.
|
|
|
|
Formalizing Abstract Algebra in Constructive Set Theory
By Xin Yu. Master's Thesis, California Institute of Technology,
2002.
|
|
|
|
Notes on the Design and Purpose of the FDL
By S. Allen. Cornell University, ongoing.
|
|
|
|
FDL: A Prototype Formal Digital Library
By S. Allen, et al. Cornell University, 2002.
|
|
|
|
Naive Computational Type Theory
By R. Constable. In Proof and System-Reliability, 2002. |
|
|
|
Reflecting Higher-Order Abstract Syntax in Nuprl
By E. Barzilay and S. Allen. TPHOLs, 2002.
|
|
|
|
Representing Nuprl Proof Objects in ACL2: toward a proof checker
for Nuprl
By J. Caldwell and J. Cowles. ACL2 Workshop, 2002.
|
|
|
|
Theory and Implementation of an Efficient Tactic-Based Logical
Framework
By Aleksey Nogin. PhD Thesis, Cornell University,
2002.
|
|
2001
|
|
|
Logical Aspects of Digital Mathematics Libraries (extended abstract)
By A. Allen, J. Caldwell, and R. Constable. MKM Workshop, 2001.
|
|
|
|
JProver: Integrating Connection-based Theorem Proving into
Interactive Proof Assistants.
By S. Schmitt, et al. IJCAR '01, 2001.
|
|
| |
|
|
