×

Found 25 Documents (Results 1–25)

Extracting general recursive program schemes in Nuprl’s type theory. (English) Zbl 1073.68571

Pettorossi, Alberto (ed.), Logic based program synthesis and transformation. 11th international workshop, LOPSTR 2001, Paphos, Cyprus, November 28–30, 2001. Selected papers. Berlin: Springer (ISBN 3-540-43915-3). Lect. Notes Comput. Sci. 2372, 233-244 (2002).
MSC:  68N30 03F35 68T15
PDFBibTeX XMLCite
Full Text: Link

Computational complexity and induction for partial computable functions in type theory. (English) Zbl 1016.03044

Sieg, Wilfried (ed.) et al., Reflections on the foundations of mathematics. Essays in honor of Solomon Feferman. Natick, MA: A K Peters. Lect. Notes Log. 15, 164-181 (2002).
Reviewer: U.Schöning (Ulm)
PDFBibTeX XMLCite

Markov’s principle for propositional type theory. (English) Zbl 0999.03053

Fribourg, Laurent (ed.), Computer science logic. 15th international workshop, CSL 2001, 10th annual conference of the EACSL, Paris, France, September 10-13, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2142, 570-584 (2001).
MSC:  03F35 03B70 03B15
PDFBibTeX XMLCite
Full Text: Link

Reflective reasoning with and between a declarative metatheory and the implementation code. (English) Zbl 0745.68092

Artificial intelligence, IJCAI-91, Proc. 12th Int. Conf., Sydney/Australia 1991, 111-117 (1991).
Reviewer: N.Curteanu (Iaşi)
MSC:  68T15 03B35 68T27 03C85
PDFBibTeX XMLCite

Finding computational content in classical proofs. (English) Zbl 0754.03040

Logical frameworks, Proc. 1st Annu. Workshop, Sophia-Antipolis/Fr. 1990, 341-362 (1991).
MSC:  03F35 03B35
PDFBibTeX XMLCite

Goal directed proof construction in type theory. (English) Zbl 0757.03008

Logical frameworks, Proc. 1st Annu. Workshop, Sophia-Antipolis/Fr. 1990, 120-148 (1991).
MSC:  03B35 68T15 03F07 03B40 03B15 03F35
PDFBibTeX XMLCite

Filter Results by …

Document Type

all top 5

Year of Publication

Main Field

all top 3

Software