Document Search Results

A simple and general theoretical account for abstract types. (English) Zbl 1266.68088

Oliveira, Marcel Vinícius Medeiros (ed.) et al., Formal methods: Foundations and applications. 12th Brazilian symposium on formal methods, SBMF 2009, Gramado, Brazil, August 19–21, 2009. Revised selected papers. Berlin: Springer (ISBN 978-3-642-10451-0/pbk). Lecture Notes in Computer Science 5902, 336-349 (2009).

MSC: 68N18

Cite Review PDF

Full Text: DOI

Xi, Hongwei

ATS/LF: A type system for constructing proofs as total functional programs. (English) Zbl 1226.68026

Benzmüller, Christoph (ed.) et al., Reasoning in simple type theory. Festschrift in honor of Peter B. Andrews on his 70th birthday. London: College Publications (ISBN 978-1-904987-70-3/pbk). Studies in Logic (London) 17. Mathematical Logic and Foundations, 443-467 (2008).

MSC: 68N18 03B70 68N30

Cite Review PDF

Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei

TPS: A theorem proving system for classical type theory. (English) Zbl 1226.03026

Benzmüller, Christoph (ed.) et al., Reasoning in simple type theory. Festschrift in honor of Peter B. Andrews on his 70th birthday. London: College Publications (ISBN 978-1-904987-70-3/pbk). Studies in Logic (London) 17. Mathematical Logic and Foundations, 367-399 (2008).

MSC: 03B35 03B15 68T15 01A75

Cite Review PDF

Xi, Hongwei

Attributive types for proof erasure. (English) Zbl 1138.68363

Miculan, Marino (ed.) et al., Types for proofs and programs. International conference, TYPES 2007, Cividale des Friuli, Italy, May 2–5, 2007. Revised selected papers. Berlin: Springer (ISBN 978-3-540-68084-0/pbk). Lecture Notes in Computer Science 4941, 188-202 (2008).

MSC: 68N30 68T15

Cite Review PDF

Full Text: DOI

Stump, Aron (ed.); Xi, Hongwei (ed.)

Proceedings of the programming languages meets program verification (PLPV 2006), Seattle, WA, USA, August 21, 2006. (English) Zbl 1273.68046

Electronic Notes in Theoretical Computer Science 174, No. 7. Amsterdam: Elsevier. 147 p., electronic only (2007).

MSC: 68-06 68N15 68Q60 00B25

Cite Review PDF

Full Text: Link

Xi, Hongwei

Dependent ML an approach to practical programming with dependent types. (English) Zbl 1125.68033

J. Funct. Program. 17, No. 2, 215-286 (2007).

MSC: 68N18 68N15

Cite Review PDF

Full Text: DOI

Chen, Chiyan; Shi, Rui; Xi, Hongwei

Implementing typeful program transformations. (English) Zbl 1096.68024

Fundam. Inform. 69, No. 1-2, 103-121 (2006).

MSC: 68N30

Cite Review PDF

Chen, Chiyan; Xi, Hongwei

Combining programming with theorem proving. (English) Zbl 1302.68241

Proceedings of the 10th ACM SIGPLAN international conference on functional programming, ICFP ’05, Tallinn, Estonia, September 26–28, 2005. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-59593-064-7). ACM SIGPLAN Notices 40, No. 9, 66-77 (2005).

MSC: 68T15 68N15

Cite Review PDF

Full Text: DOI

Cui, Sa; Donnelly, Kevin; Xi, Hongwei

ATS: A language that combines programming with theorem proving. (English) Zbl 1171.68421

Gramlich, Bernhard (ed.), Frontiers of combining systems. 5th international workshop, FroCos 2005, Vienna, Austria, September 19–21, 2005. Proceedings. Berlin: Springer (ISBN 3-540-29051-6/pbk). Lecture Notes in Computer Science 3717. Lecture Notes in Artificial Intelligence, 310-320 (2005).

MSC: 68N30 68T15

Cite Review PDF

Full Text: DOI

Chen, Chiyan; Xi, Hongwei

Meta-programming through typeful code representation. (English) Zbl 1085.68547

J. Funct. Program. 15, No. 6, 797-835 (2005).

MSC: 68N18

Cite Review PDF

Full Text: DOI

Xi, Hongwei

Applied type system (extended abstract). (English) Zbl 1100.03518

Berardi, Stefano (ed.) et al., Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 – May 4, 2003. Revised selected papers. Berlin: Springer (ISBN 3-540-22164-6/pbk). Lecture Notes in Computer Science 3085, 394-408 (2004).

MSC: 03B70 68N18 68N30

Cite Review PDF

Full Text: DOI

Xi, Hongwei; Chen, Chiyan; Chen, Gang

Guarded recursive datatype constructors. (English) Zbl 1321.68161

Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’03, New Orleans, LA, USA, January 15–17, 2003. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-628-5). 224-235 (2003).

MSC: 68N18

Cite Review PDF

Full Text: DOI

Chen, Chiyan; Xi, Hongwei

Meta-programming through typeful code representation. (English) Zbl 1315.68038

Proceedings of the 8th ACM SIGPLAN international conference on functional programming, ICFP ’03, Uppsala, Sweden, August 25–29, 2003. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-756-7). ACM SIGPLAN Notices 38, No. 9, 275-286 (2003).

MSC: 68N15 68N30

Cite Review PDF

Full Text: DOI

Xi, Hongwei

Dependent types for program termination verification. (English) Zbl 1041.68059

High.-Order Symb. Comput. 15, No. 1, 91-131 (2002).

MSC: 68Q60

Cite Review PDF

Full Text: DOI

Xi, Hongwei; Harper, Robert

A dependently typed assembly language. (English) Zbl 1323.68084

Proceedings of the 6th ACM SIGPLAN international conference on functional programming, ICFP ’01, Florence, Italy, September 3–5, 2001. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-415-0). ACM SIGPLAN Notices 36, No. 10, 169-180 (2001).

MSC: 68N15 68N18

Cite Review PDF

Full Text: DOI

Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei

TPS: A theorem-proving system for classical type theory. (English) Zbl 0858.03017

J. Autom. Reasoning 16, No. 3, 321-353 (1996).

Reviewer: M.P.Bonacina (Iowa City)

MSC: 03B35 03B15 68T15

Cite Review PDF

Full Text: DOI

Found 16 Documents (Results 1–16)

A simple and general theoretical account for abstract types. (English) Zbl 1266.68088

ATS/LF: A type system for constructing proofs as total functional programs. (English) Zbl 1226.68026

TPS: A theorem proving system for classical type theory. (English) Zbl 1226.03026

Attributive types for proof erasure. (English) Zbl 1138.68363

Proceedings of the programming languages meets program verification (PLPV 2006), Seattle, WA, USA, August 21, 2006. (English) Zbl 1273.68046

Dependent ML an approach to practical programming with dependent types. (English) Zbl 1125.68033

Implementing typeful program transformations. (English) Zbl 1096.68024

Combining programming with theorem proving. (English) Zbl 1302.68241

ATS: A language that combines programming with theorem proving. (English) Zbl 1171.68421

Meta-programming through typeful code representation. (English) Zbl 1085.68547

Applied type system (extended abstract). (English) Zbl 1100.03518

Guarded recursive datatype constructors. (English) Zbl 1321.68161

Meta-programming through typeful code representation. (English) Zbl 1315.68038

Dependent types for program termination verification. (English) Zbl 1041.68059

A dependently typed assembly language. (English) Zbl 1323.68084

TPS: A theorem-proving system for classical type theory. (English) Zbl 0858.03017

Filter Results by …

Document Type

Author

Serial

Year of Publication

Main Field

Software