×

Found 29 Documents (Results 1–29)

A computational interpretation of forcing in type theory. (English) Zbl 1312.03021

Dybjer, Peter (ed.) et al., Epistemology versus ontology. Essays on the philosophy and foundations of mathematics in honour of Per Martin-Löf. Based on the conference, “Philosophy and foundations of mathematics: Epistemological and ontological aspects”, Uppsala, Sweden, May 5–8, 2009. Dordrecht: Springer (ISBN 978-94-007-4434-9/hbk; 978-94-007-4435-6/ebook). Logic, Epistemology, and the Unity of Science 27, 203-213 (2012).
MSC:  03B15 03B40 03E40 68N18
PDFBibTeX XMLCite
Full Text: DOI Link

Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. (English) Zbl 1112.68346

Urzyczyn, Paweł (ed.), Typed lambda calculi and applications. 7th international conference, TLCA 2005, Nara, Japan, April 21–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25593-1/pbk). Lecture Notes in Computer Science 3461, 23-38 (2005).
MSC:  68N30 03B40 68N18
PDFBibTeX XMLCite
Full Text: DOI

A logical framework with dependently typed records. (English) Zbl 1052.68018

Hofmann, Martin (ed.), Typed lambda calculi and applications. 6th international conference, TLCA 2003, Valencia, Spain, June 10–12, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40332-9/pbk). Lect. Notes Comput. Sci. 2701, 105-119 (2003).
MSC:  68N18 03B70 03B40 68Q55 68Q60 68Q65 68T15
PDFBibTeX XMLCite
Full Text: Link

An introduction to dependent type theory. (English) Zbl 1065.68025

Barthe, Gilles (ed.) et al., Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9–15, 2000. Advanced lectures. Berlin: Springer (ISBN 3-540-44044-5). Lect. Notes Comput. Sci. 2395, 1-41 (2002).
PDFBibTeX XMLCite
Full Text: Link

A new paradox in type theory. (English) Zbl 0821.03005

Prawitz, D. (ed.) et al., Logic, methodology and philosophy of science IX. Proceedings of the ninth international congress of logic, methodology and philosophy of science, Uppsala, Sweden, August 7-14, 1991. Amsterdam: North-Holland. Stud. Logic Found. Math. 134, 555-570 (1994).
MSC:  03B40 03B15
PDFBibTeX XMLCite

An algorithm for testing conversion in type theory. (English) Zbl 0754.03041

Logical frameworks, Proc. 1st Annu. Workshop, Sophia-Antipolis/Fr. 1990, 255-279 (1991).
MSC:  03F35 03B40 03B70
PDFBibTeX XMLCite

Filter Results by …

Document Type

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software