Sciweavers

DLOG
2010
13 years 9 months ago
Logic for Modeling Product Structure
A fragment of type theory with OWL class constructions for types and binary properties is used to formalize SysML Structural Block Diagram models. A structural SysML block diagram ...
Henson Graves
MST
2007
168views more  MST 2007»
13 years 10 months ago
Productivity of Edalat-Potts Exact Arithmetic in Constructive Type Theory
In this work we focus on a formalisation of the algorithms of lazy exact arithmetic `a la Edalat–Potts in type theory. We choose the constructive type theory extended with coind...
Milad Niqui
BSL
2002
113views more  BSL 2002»
13 years 11 months ago
Types in logic and mathematics before 1940
Abstract. In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910
Fairouz Kamareddine, Twan Laan, Rob Nederpelt
ENTCS
2007
102views more  ENTCS 2007»
13 years 11 months ago
Encoding Functional Relations in Scunak
We describe how a set-theoretic foundation for mathematics can be encoded in the new system Scunak. We then discuss an encoding of the construction of functions as functional relat...
Chad E. Brown
JAPLL
2006
79views more  JAPLL 2006»
13 years 11 months ago
Innovations in computational type theory using Nuprl
For twenty years the Nuprl ("new pearl") system has been used to develop software systems and formal theories of computational mathematics. It has also been used to expl...
Stuart F. Allen, Mark Bickford, Robert L. Constabl...
JAPLL
2006
87views more  JAPLL 2006»
13 years 11 months ago
Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
This paper presents Automath encodings (which also are valid in LF/P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to f...
Freek Wiedijk
ENTCS
2006
125views more  ENTCS 2006»
13 years 11 months ago
Formalizing Type Operations Using the "Image" Type Constructor
In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized...
Aleksey Nogin, Alexei Kopylov
ENTCS
2008
94views more  ENTCS 2008»
13 years 11 months ago
A Logical Framework with Explicit Conversions
The type theory P corresponds to the logical framework LF. In this paper we present H, a variant of P where convertibility is not implemented by means of the customary conversion ...
Herman Geuvers, Freek Wiedijk
ENTCS
2008
128views more  ENTCS 2008»
13 years 11 months ago
Towards Formalizing Categorical Models of Type Theory in Type Theory
This note is about work in progress on the topic of "internal type theory" where we investigate the internal formalization of the categorical metatheory of constructive ...
Alexandre Buisse, Peter Dybjer
CORR
2010
Springer
158views Education» more  CORR 2010»
13 years 11 months ago
A Minimal Propositional Type Theory
Propositional type theory, first studied by Henkin, is the restriction of simple type theory to a single base type that is interpreted as the set of the two truth values. We show ...
Mark Kaminski, Gert Smolka