Ulf Norell - researchr profile publications

researchr

You are not signed in
Sign in
Sign up

[Clear Filters]

Publications tagged type theory

Verifying haskell programs using constructive type theoryAndreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell. haskell 2005: 62-73 [doi]

Proving Theorems of Type Theory Automatically with TPSPeter B. Andrews. AAAI 2005: 1676-1677

Certifying circuits in Type TheorySolange Coupet-Grimal, Line Jakubiec. fac, 16(4):352-373, 2004. [doi]

Computational adequacy for recursive types in models of intuitionistic set theoryAlex K. Simpson. APAL, 130(1-3):207-275, 2004. [doi]

Behavioral Compatibility of Self-Typed TheoriesSuad Alagic, Svetlana Kouznetsova. ECOOP 2002: 585-608 [doi]

Equational Theories Generated By Hypersubstitutions of Type (n)Klaus Denecke, Jörg Koppitz, Staszek Niwczyk. ijac, 12(6):867-876, 2002. [doi]

Computational Adequacy for Recursive Types in Models of Intuitionistic Set TheoryAlex K. Simpson. lics 2002: 287-298 [doi]

General Recursion in Type TheoryAna Bove. TYPES 2003: 39-58 [doi]

Subsets, Quotients and Partial Functions in Martin-Löf s Type TheoryJesper Carlström. TYPES 2003: 78-94 [doi]

The Simple Type Theory of Normalization by EvaluationRené Vestergaard. TCS, 57:163-183, 2001. [doi]

Simple General Recursion in Type TheoryAna Bove. njc, 8(1):22-42, 2001.

Classical Type TheoryPeter B. Andrews. In John Alan Robinson, Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes). pages 965-1007, Elsevier and MIT Press, 2001.

Extracting General Recursive Program Schemes in Nuprl s Type TheoryJames L. Caldwell. LOPSTR 2001: 233-244 [doi]

What Entailment Can do for Type TheoryRobert K. Meyer. icalp 2000: 355-356

Formalizing the Halting Problem in a Constructive Type TheoryKristofer Johannisson. TYPES 2002: 145-159 [doi]

Lascar Strong Types in Some Simple TheoriesSteven Buechler. JSYML, 64(2):817-824, 1999.

Finding Zeros of Analytic Functions: alpha Theory for Secant Type MethodsJean-Claude Yakoubsohn. jc, 15(2):239-281, 1999. [doi]

Structural Recursive Definitions in Type TheoryEduardo Giménez. icalp 1998: 397-408 [doi]

A Type Theory for Cyclic StrctureIzumi Takeuti. FLOPS 1998: 207-226

Typing Algorithm in Type Theory with InheritanceAmokrane Saïbi. POPL 1997: 292-301 [doi]

A Type-Theoretic Interpretation of Constructive Domain TheoryMichael Hedberg. JAR, 16(3):369-425, 1996.

An Implementation of the Heine-Borel Covering Theorem in Type TheoryJan Cederquist. TYPES 1998: 46-65

Decidability in Intuitionistic Type Theory is Functionally DecidableSilvio Valentini. mlq, 42:300-304, 1996.

Hybrid Partial-Total Type TheoryScott F. Smith. ijfcs, 6(3):235-263, 1995.

Theories = Signatures + Propositions Used as TypesStephan A. Missura. AISC 1995: 144-155

Strongly-Typed Theory of Structures and BehavioursKeith Hanna, Neil Daeche. charme 1993: 39-54

Universes in the Theory of Types and NamesMarkus Marzetta. csl 1993: 340-351

A Classical Type Theory with Transfinite TypesGarrel Pottinger. tphol 1993: 81-94

An Intuitionistic Theory of Types with Assumptions of High-Arity VariablesAnnalisa Bossi, Silvio Valentini. APAL, 57(2):93-149, 1992.

Oyster-2: Bringing Type Theory into PracticeChristian Horn. ifip 1992: 49-56

Partial Functions in Type TheoryFrançois Lepage. ndjfl, 33(4):493-516, 1992.

Type-Free Property Theory, Exemplification and Russell s ParadoxFrancesco Orilia. ndjfl, 32(3):432-447, 1991.

Extracting Recursive Programs in Type TheoryScott F. Smith. amast 1992: 341-349

Resolution and Type TheoryLeen Helmink. SCP, 17(1-3):119-138, 1991.

On a Hierarchy of File Types and a Tower of Their TheoriesAndrzej Salwicki. mfcs 1991: 47-63

Sentences of Type Theory: The Only Sentences Preserved Under IsomorphismsM. Victoria Marshall, Rolando Chuaqui. JSYML, 56(3):932-948, 1991.

Resolution and Type TheoryLeen Helmink. ESOP 1990: 197-211

A Set Constructor for Inductive Sets in Martin-Löf s Type TheoryKent Petersson, Dan Synek. ctcs 1989: 128-140

The Strength of the Subset Type in Martin-Löf s Type TheoryAnne Salvesen, Jan M. Smith. lics 1988: 384-391

The Independence of Peano s Fourth Axiom from Martin-Lof s Type Theory Without UniversesJan M. Smith. JSYML, 53(3):840-845, 1988.

On the Syntax of Martin-Löf s Type TheoriesA. S. Troelstra. TCS, 51:1-26, 1987.

Arithmetic and the Theory of TypesMaurice Boffa. JSYML, 49(2):621-624, 1984.

An Interpretation of Martin-Lof s Type Theory in a Type-Free Theory of PropositionsJan M. Smith. JSYML, 49(3):730-753, 1984.

A Lattice of Interpretability Types of TheoriesJan Mycielski. JSYML, 42(2):297-305, 1977.

Theorem Proving in Type TheoryPeter B. Andrews, Eve Longini Cohen. IJCAI 1977: 566-566

Natural Models and Ackermann-Type Set TheoriesJohn Lake. JSYML, 40(2):151-158, 1975.

On an Ackermann-Type Set TheoryJohn Lake. JSYML, 38(3):410-412, 1973.

Syntactical and Semantical Properties of Simple Type TheoryKurt Schutte. JSYML, 25(4):305-326, 1960.

A Formulation of the Simple Theory of TypesAlonzo Church. JSYML, 5(2):56-68, 1940.

On the Theory of TypesW. V. Quine. JSYML, 3(4):125-139, 1938.

runs on WebDSL