Moczydłowski, Wojciech Unifying sets and programs via dependent types. (English) Zbl 1238.68050 Ann. Pure Appl. Logic 163, No. 7, 789-808 (2012). MSC: 68N30 03E70 03F50 PDFBibTeX XMLCite \textit{W. Moczydłowski}, Ann. Pure Appl. Logic 163, No. 7, 789--808 (2012; Zbl 1238.68050) Full Text: DOI
Constable, Robert L.; Moczydlowski, Wojciech Extracting programs from constructive HOL proofs via IZF set-theoretic semantics. (English) Zbl 1147.03013 Log. Methods Comput. Sci. 4, No. 3, Paper 5, 17 p. (2008). MSC: 03B70 03B15 03B35 03E70 68N30 68T15 PDFBibTeX XMLCite \textit{R. L. Constable} and \textit{W. Moczydlowski}, Log. Methods Comput. Sci. 4, No. 3, Paper 5, 17 p. (2008; Zbl 1147.03013) Full Text: DOI
Moczydłowski, Wojciech A normalizing intuitionistic set theory with inaccessible sets. (English) Zbl 1125.03038 Log. Methods Comput. Sci. 3, No. 3, Paper 6, 31 p. (2007). MSC: 03E70 03B40 03F50 03B35 03B70 PDFBibTeX XMLCite \textit{W. Moczydłowski}, Log. Methods Comput. Sci. 3, No. 3, Paper 6, 31 p. (2007; Zbl 1125.03038) Full Text: DOI
Coquand, Thierry; Pollack, Randy; Takeyama, Makoto A logical framework with dependently typed records. (English) Zbl 1095.03017 Fundam. Inform. 65, No. 1-2, 113-134 (2005). Reviewer: Neculai Curteanu (Iaşi) MSC: 03B70 68N18 03F35 03B35 03B40 68Q65 68Q60 68Q55 68T15 68T20 PDFBibTeX XMLCite \textit{T. Coquand} et al., Fundam. Inform. 65, No. 1--2, 113--134 (2005; Zbl 1095.03017)
Caldwell, James L. 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 \textit{J. L. Caldwell}, Lect. Notes Comput. Sci. 2372, 233--244 (2002; Zbl 1073.68571) Full Text: Link
Constable, Robert L.; Crary, Karl 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) MSC: 03D65 03D15 03F35 03B70 PDFBibTeX XMLCite \textit{R. L. Constable} and \textit{K. Crary}, Lect. Notes Log. 15, 164--181 (2002; Zbl 1016.03044)
Kopylov, Alexei; Nogin, Aleksey 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 \textit{A. Kopylov} and \textit{A. Nogin}, Lect. Notes Comput. Sci. 2142, 570--584 (2001; Zbl 0999.03053) Full Text: Link
Kamareddine, Fairouz; Laan, Twan A correspondence between Martin-Löf type theory, the ramified theory of types and pure type systems. (English) Zbl 0977.03011 J. Logic Lang. Inf. 10, No. 3, 375-402 (2001). MSC: 03B35 03F35 PDFBibTeX XMLCite \textit{F. Kamareddine} and \textit{T. Laan}, J. Logic Lang. Inf. 10, No. 3, 375--402 (2001; Zbl 0977.03011) Full Text: DOI
Maietti, Maria Emilia About effective quotients in constructive type theory. (English) Zbl 0943.03053 Altenkirch, Thorsten (ed.) et al., Types for proofs and programs. International workshop, TYPES ’98. Kloster Irsee, Germany, March 27-31, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1657, 164-178 (1999). MSC: 03F65 03F35 03E70 PDFBibTeX XMLCite \textit{M. E. Maietti}, Lect. Notes Comput. Sci. 1657, 164--178 (1999; Zbl 0943.03053)
Poll, Erik; Zwanenburg, Jan A logic for abstract data types as existential types. (English) Zbl 0931.03026 Girard, Jean-Yves (ed.), Typed lambda calculi and applications. 4th international conference, TLCA ’99. L’Aquila, Italy, April 7–9, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1581, 310-324 (1999). MSC: 03B40 68Q65 03B70 PDFBibTeX XMLCite \textit{E. Poll} and \textit{J. Zwanenburg}, Lect. Notes Comput. Sci. 1581, 310--324 (1999; Zbl 0931.03026)
Constable, Robert L. The structure of Nuprl’s type theory. (English) Zbl 0876.03010 Schwichtenberg, Helmut (ed.), Logic of computation. Proceedings of the NATO ASI. Marktoberdorf, Germany. July 25–August 6, 1995. Berlin: Springer. NATO ASI Ser., Ser. F, Comput. Syst. Sci. 157, 123-155 (1997). MSC: 03B35 03F35 03F03 03B70 PDFBibTeX XMLCite \textit{R. L. Constable}, NATO ASI Ser., Ser. F, Comput. Syst. Sci. 157, 123--155 (1997; Zbl 0876.03010)
Turner, Raymond Reading between the lines in constructive type theory. (English) Zbl 0882.03058 J. Log. Comput. 7, No. 2, 229-250 (1997). MSC: 03F50 03F35 03B70 PDFBibTeX XMLCite \textit{R. Turner}, J. Log. Comput. 7, No. 2, 229--250 (1997; Zbl 0882.03058) Full Text: DOI
Takayama, Yukihide \(QPC_ 2\): A constructive calculus with parameterized specifications. (English) Zbl 0804.68085 J. Symb. Comput. 15, No. 5-6, 641-672 (1993). MSC: 68Q60 68Q65 68N17 03F35 03F50 68T15 PDFBibTeX XMLCite \textit{Y. Takayama}, J. Symb. Comput. 15, No. 5--6, 641--672 (1993; Zbl 0804.68085) Full Text: DOI
Harper, Robert Constructing type systems over an operational semantics. (English) Zbl 0766.68088 J. Symb. Comput. 14, No. 1, 71-84 (1992). MSC: 68Q55 03F35 PDFBibTeX XMLCite \textit{R. Harper}, J. Symb. Comput. 14, No. 1, 71--84 (1992; Zbl 0766.68088) Full Text: DOI
Giunchiglia, Fausto; Traverso, Paolo 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 \textit{F. Giunchiglia} and \textit{P. Traverso}, in: IJCAI 91, Proceedings of the 12th International Conference on Artificial Intelligence. Sydney, Australia, 24-30 August 1991. Vol. 1-2. San Mateo, CA: Morgan Kaufmann Publ.. 111--117 (1991; Zbl 0745.68092)
Constable, Robert; Murthy, Chet Finding computational content in classical proofs. (English) Zbl 0754.03040 Logical frameworks, Proc. 1st Annu. Workshop, Sophia-Antipolis/Fr. 1990, 341-362 (1991). Reviewer: P.Štěpánek (Praha) MSC: 03F35 03B35 PDFBibTeX XMLCite \textit{R. Constable} and \textit{C. Murthy}, in: Logical frameworks. Proceedings of the first annual workshop ''Logical frameworks: design, implementation and experiment'', held in Sophia- Antipolis, France, May 7-11, 1990. Cambridge etc.: Cambridge University Press. 341--362 (1991; Zbl 0754.03040)
Helmink, Leen; Ahn, René Goal directed proof construction in type theory. (English) Zbl 0757.03008 Logical frameworks, Proc. 1st Annu. Workshop, Sophia-Antipolis/Fr. 1990, 120-148 (1991). Reviewer: L.State (Bucureşti) MSC: 03B35 68T15 03F07 03B40 03B15 03F35 PDFBibTeX XMLCite \textit{L. Helmink} and \textit{R. Ahn}, in: Logical frameworks. Proceedings of the first annual workshop ''Logical frameworks: design, implementation and experiment'', held in Sophia- Antipolis, France, May 7-11, 1990. Cambridge etc.: Cambridge University Press. 120--148 (1991; Zbl 0757.03008)
Luo, Zhaohui A higher-order calculus and theory abstraction. (English) Zbl 0719.03004 Inf. Comput. 90, No. 1, 107-137 (1991). Reviewer: Z.Luo MSC: 03B15 03F35 68Q60 03B70 PDFBibTeX XMLCite \textit{Z. Luo}, Inf. Comput. 90, No. 1, 107--137 (1991; Zbl 0719.03004) Full Text: DOI
Howe, Douglas J. Equality in lazy computation systems. (English) Zbl 0716.68065 Logic in computer science, Proc. 4th Annual Symp., Pacific Grove/CA (USA) 1989, 198-203 (1989). MSC: 68Q60 68N15 03F35 68Q05 03B40 PDFBibTeX XML
Backhouse, Roland; Chisholm, Paul; Malcolm, Grant; Saaman, Erik Do-it-yourself type theory. (English) Zbl 0697.68020 Formal Aspects Comput. 1, No. 1, 19-84 (1989). MSC: 68Q60 68P05 03F35 PDFBibTeX XMLCite \textit{R. Backhouse} et al., Formal Asp. Comput. 1, No. 1, 19--84 (1989; Zbl 0697.68020) Full Text: DOI
Smith, Jan M. Propositional functions and families of types. (English) Zbl 0694.03038 Notre Dame J. Formal Logic 30, No. 3, 442-458 (1989). Reviewer: Li Xiang MSC: 03F35 68Q65 68Q60 PDFBibTeX XMLCite \textit{J. M. Smith}, Notre Dame J. Formal Logic 30, No. 3, 442--458 (1989; Zbl 0694.03038) Full Text: DOI
Jäger, Gerhard Induction in the elementary theory of types and names. (English) Zbl 0693.03039 Computer science logic, 1st Workshop, CSL ’87, Karlsruhe/FRG 1987, Lect. Notes Comput. Sci. 329, 118-128 (1988). Reviewer: A.Tauts MSC: 03F35 PDFBibTeX XML
Howe, Douglas J. Computational metatheory in Nuprl. (English) Zbl 0646.03010 Automated deduction, Proc. 9th Int. Conf., Argonne/Ill. 1988, Lect. Notes Comput. Sci. 310, 238-257 (1988). MSC: 03B35 68T15 03F35 PDFBibTeX XML
Troelstra, A. S. On the syntax of Martin-Löf’s type theories. (English) Zbl 0638.03056 Theor. Comput. Sci. 51, 1-26 (1987). Reviewer: A.S.Troelstra MSC: 03F35 03F50 03F05 PDFBibTeX XMLCite \textit{A. S. Troelstra}, Theor. Comput. Sci. 51, 1--26 (1987; Zbl 0638.03056) Full Text: DOI
Paulson, Lawrence C. Constructing recursion operators in intuitionistic type theory. (English) Zbl 0631.03045 J. Symb. Comput. 2, 325-355 (1986). Reviewer: G.Kreisel MSC: 03F35 68Q65 68T15 PDFBibTeX XMLCite \textit{L. C. Paulson}, J. Symb. Comput. 2, 325--355 (1986; Zbl 0631.03045) Full Text: DOI