00960nam2 22002533i 450 SUN009578620140127032133.70520131028d1948 |0itac50 baitaIT|||| |||||ˆ2: Le ‰fontiLodovico Barassi2. ed. aumentataMilanoGiuffrè1948XIV, P. 57626 cm. - Fondo Tribunale di Napoli.001SUN00399372001 ˆLa ‰teoria generale delle obbligazioniLodovico Barassi2210 MilanoGiuffrè215 v.25 cm.MilanoSUNL000284Barassi, LodovicoSUNV0325863043GiuffrèSUNV001757650ITSOL20181231RICASUN0095786UFFICIO DI BIBLIOTECA DEL DIPARTIMENTO DI GIURISPRUDENZA00CONS FTA.142 (2) 00FTN7566 20131028 Fonti927343UNICAMPANIA04424nam 22007455 450 99646577170331620200702125330.03-540-47770-510.1007/3-540-60579-7(CKB)1000000000234368(SSID)ssj0000327463(PQKBManifestationID)11247114(PQKBTitleCode)TC0000327463(PQKBWorkID)10297592(PQKB)10616989(DE-He213)978-3-540-47770-9(PPN)155197851(EXLCZ)99100000000023436820121227d1995 u| 0engurnn|008mamaatxtccrTypes for Proofs and Programs[electronic resource] International Workshop TYPES '94, Bastad, Sweden, June 6-10, 1994. Selected Papers /edited by Peter Dybjer, Bengt Nordström, Jan Smith1st ed. 1995.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,1995.1 online resource (X, 210 p.) Lecture Notes in Computer Science,0302-9743 ;996Bibliographic Level Mode of Issuance: Monograph3-540-60579-7 Communicating contexts: A pragmatic approach to information exchange -- A short and flexible proof of strong normalization for the calculus of constructions -- Codifying guarded definitions with recursive schemes -- The metatheory of UTT -- A user's friendly syntax to define recursive functions as typed ?-terms -- I/O automata in Isabelle/HOL -- A concrete final coalgebra theorem for ZF set theory -- On extensibility of proof checkers -- Syntactic categories in the language of mathematics -- Formalization of a ?-calculus with explicit substitutions in Coq.This book presents a strictly refereed collection of revised full papers selected from the papers accepted for the TYPES '94 Workshop, held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs in Bastad, Sweden, in June 1994. The 10 papers included address various aspects of developing computer-assisted proofs and programs using a logical framework. Type theory and three logical frameworks based on it are dealt with: ALF, Coq, and LEGO; other topics covered are metatheory, the Isabelle system, 2-calculus, proof checkers, and ZF set theory.Lecture Notes in Computer Science,0302-9743 ;996Software engineeringMathematical logicComputer logicProgramming languages (Electronic computers)Artificial intelligenceSoftware Engineering/Programming and Operating Systemshttps://scigraph.springernature.com/ontologies/product-market-codes/I14002Mathematical Logic and Formal Languageshttps://scigraph.springernature.com/ontologies/product-market-codes/I16048Logics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XProgramming Languages, Compilers, Interpretershttps://scigraph.springernature.com/ontologies/product-market-codes/I14037Artificial Intelligencehttps://scigraph.springernature.com/ontologies/product-market-codes/I21000Mathematical Logic and Foundationshttps://scigraph.springernature.com/ontologies/product-market-codes/M24005Software engineering.Mathematical logic.Computer logic.Programming languages (Electronic computers).Artificial intelligence.Software Engineering/Programming and Operating Systems.Mathematical Logic and Formal Languages.Logics and Meanings of Programs.Programming Languages, Compilers, Interpreters.Artificial Intelligence.Mathematical Logic and Foundations.005.13/1Dybjer Peteredthttp://id.loc.gov/vocabulary/relators/edtNordström Bengtedthttp://id.loc.gov/vocabulary/relators/edtSmith Janedthttp://id.loc.gov/vocabulary/relators/edtInternational Workshop TYPES '94BOOK996465771703316Types for Proofs and Programs771867UNISA